src/HOL/Analysis/Determinants.thy
changeset 68833 fde093888c16
parent 68263 e4e536a71e3d
child 69064 5840724b1d71
--- a/src/HOL/Analysis/Determinants.thy	Mon Aug 27 22:58:36 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Tue Aug 28 13:28:39 2018 +0100
@@ -10,40 +10,40 @@
   "HOL-Library.Permutations"
 begin
 
-subsection \<open>Trace\<close>
+subsection%important  \<open>Trace\<close>
 
-definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
+definition%important  trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
   where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
 
-lemma trace_0: "trace (mat 0) = 0"
+lemma%unimportant  trace_0: "trace (mat 0) = 0"
   by (simp add: trace_def mat_def)
 
-lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
+lemma%unimportant  trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
   by (simp add: trace_def mat_def)
 
-lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
+lemma%unimportant  trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
   by (simp add: trace_def sum.distrib)
 
-lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
+lemma%unimportant  trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
   by (simp add: trace_def sum_subtractf)
 
-lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
+lemma%important  trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
   apply (simp add: trace_def matrix_matrix_mult_def)
   apply (subst sum.swap)
   apply (simp add: mult.commute)
   done
 
-subsubsection \<open>Definition of determinant\<close>
+subsubsection%important  \<open>Definition of determinant\<close>
 
-definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
+definition%important  det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
   "det A =
     sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
       {p. p permutes (UNIV :: 'n set)}"
 
 text \<open>Basic determinant properties\<close>
 
-lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
-proof -
+lemma%important  det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
+proof%unimportant -
   let ?di = "\<lambda>A i j. A$i$j"
   let ?U = "(UNIV :: 'n set)"
   have fU: "finite ?U" by simp
@@ -80,7 +80,7 @@
     by (subst sum_permutations_inverse) (blast intro: sum.cong)
 qed
 
-lemma det_lowerdiagonal:
+lemma%unimportant  det_lowerdiagonal:
   fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
   assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
@@ -107,11 +107,11 @@
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma det_upperdiagonal:
+lemma%important  det_upperdiagonal:
   fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
   assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
-proof -
+proof%unimportant -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
   let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
@@ -134,11 +134,11 @@
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma det_diagonal:
+lemma%important  det_diagonal:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
   shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)"
-proof -
+proof%unimportant -
   let ?U = "UNIV:: 'n set"
   let ?PU = "{p. p permutes ?U}"
   let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
@@ -161,13 +161,13 @@
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
+lemma%unimportant  det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
   by (simp add: det_diagonal mat_def)
 
-lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
+lemma%unimportant  det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
   by (simp add: det_def prod_zero power_0_left)
 
-lemma det_permute_rows:
+lemma%unimportant  det_permute_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes p: "p permutes (UNIV :: 'n::finite set)"
   shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
@@ -204,11 +204,11 @@
     done
 qed
 
-lemma det_permute_columns:
+lemma%important  det_permute_columns:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes p: "p permutes (UNIV :: 'n set)"
   shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
-proof -
+proof%unimportant -
   let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
   let ?At = "transpose A"
   have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))"
@@ -220,7 +220,7 @@
     by simp
 qed
 
-lemma det_identical_columns:
+lemma%unimportant  det_identical_columns:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes jk: "j \<noteq> k"
     and r: "column j A = column k A"
@@ -300,24 +300,24 @@
   finally show "det A = 0" by simp
 qed
 
-lemma det_identical_rows:
+lemma%unimportant  det_identical_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"
   assumes ij: "i \<noteq> j" and r: "row i A = row j A"
   shows "det A = 0"
   by (metis column_transpose det_identical_columns det_transpose ij r)
 
-lemma det_zero_row:
+lemma%unimportant  det_zero_row:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
   by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
 
-lemma det_zero_column:
+lemma%unimportant  det_zero_column:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0"
   unfolding atomize_conj atomize_imp
   by (metis det_transpose det_zero_row row_transpose)
 
-lemma det_row_add:
+lemma%unimportant  det_row_add:
   fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
     det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
@@ -358,7 +358,7 @@
     by (simp add: field_simps)
 qed auto
 
-lemma det_row_mul:
+lemma%unimportant  det_row_mul:
   fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
     c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
@@ -395,7 +395,7 @@
     by (simp add: field_simps)
 qed auto
 
-lemma det_row_0:
+lemma%unimportant  det_row_0:
   fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
   shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
   using det_row_mul[of k 0 "\<lambda>i. 1" b]
@@ -403,11 +403,11 @@
   apply (simp only: vector_smult_lzero)
   done
 
-lemma det_row_operation:
+lemma%important  det_row_operation:
   fixes A :: "'a::{comm_ring_1}^'n^'n"
   assumes ij: "i \<noteq> j"
   shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
-proof -
+proof%unimportant -
   let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
   have th: "row i ?Z = row j ?Z" by (vector row_def)
   have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
@@ -417,7 +417,7 @@
     by simp
 qed
 
-lemma det_row_span:
+lemma%unimportant  det_row_span:
   fixes A :: "'a::{field}^'n^'n"
   assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}"
   shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
@@ -449,10 +449,10 @@
     unfolding scalar_mult_eq_scaleR .
 qed
 
-lemma matrix_id [simp]: "det (matrix id) = 1"
+lemma%unimportant  matrix_id [simp]: "det (matrix id) = 1"
   by (simp add: matrix_id_mat_1)
 
-lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
+lemma%important  det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
   apply (subst det_diagonal)
    apply (auto simp: matrix_def mat_def)
   apply (simp add: cart_eq_inner_axis inner_axis_axis)
@@ -463,7 +463,7 @@
   exact duplicates by considering the rows/columns as a set.
 \<close>
 
-lemma det_dependent_rows:
+lemma%unimportant  det_dependent_rows:
   fixes A:: "'a::{field}^'n^'n"
   assumes d: "vec.dependent (rows A)"
   shows "det A = 0"
@@ -491,23 +491,23 @@
   qed
 qed
 
-lemma det_dependent_columns:
+lemma%unimportant  det_dependent_columns:
   assumes d: "vec.dependent (columns (A::real^'n^'n))"
   shows "det A = 0"
   by (metis d det_dependent_rows rows_transpose det_transpose)
 
 text \<open>Multilinearity and the multiplication formula\<close>
 
-lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
+lemma%unimportant  Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
   by auto
 
-lemma det_linear_row_sum:
+lemma%unimportant  det_linear_row_sum:
   assumes fS: "finite S"
   shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
     sum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
   using fS  by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong)
 
-lemma finite_bounded_functions:
+lemma%unimportant  finite_bounded_functions:
   assumes fS: "finite S"
   shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
 proof (induct k)
@@ -532,14 +532,14 @@
 qed
 
 
-lemma det_linear_rows_sum_lemma:
+lemma%important  det_linear_rows_sum_lemma:
   assumes fS: "finite S"
     and fT: "finite T"
   shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
     sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
       {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
   using fT
-proof (induct T arbitrary: a c set: finite)
+proof%unimportant (induct T arbitrary: a c set: finite)
   case empty
   have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
     by vector
@@ -577,7 +577,7 @@
        (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff)
 qed
 
-lemma det_linear_rows_sum:
+lemma%unimportant  det_linear_rows_sum:
   fixes S :: "'n::finite set"
   assumes fS: "finite S"
   shows "det (\<chi> i. sum (a i) S) =
@@ -589,12 +589,12 @@
   show ?thesis by simp
 qed
 
-lemma matrix_mul_sum_alt:
+lemma%unimportant  matrix_mul_sum_alt:
   fixes A B :: "'a::comm_ring_1^'n^'n"
   shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
   by (vector matrix_matrix_mult_def sum_component)
 
-lemma det_rows_mul:
+lemma%unimportant  det_rows_mul:
   "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
     prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
 proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong)
@@ -612,10 +612,10 @@
     by (simp add: field_simps)
 qed rule
 
-lemma det_mul:
+lemma%important  det_mul:
   fixes A B :: "'a::comm_ring_1^'n^'n"
   shows "det (A ** B) = det A * det B"
-proof -
+proof%unimportant -
   let ?U = "UNIV :: 'n set"
   let ?F = "{f. (\<forall>i \<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
   let ?PU = "{p. p permutes ?U}"
@@ -712,12 +712,12 @@
 qed
 
 
-subsection \<open>Relation to invertibility\<close>
+subsection%important \<open>Relation to invertibility\<close>
 
-lemma invertible_det_nz:
+lemma%important  invertible_det_nz:
   fixes A::"'a::{field}^'n^'n"
   shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
-proof (cases "invertible A")
+proof%unimportant (cases "invertible A")
   case True
   then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1"
     unfolding invertible_right_inverse by blast
@@ -748,7 +748,7 @@
 qed
 
 
-lemma det_nz_iff_inj_gen:
+lemma%unimportant  det_nz_iff_inj_gen:
   fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear ( *s) ( *s) f"
   shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
@@ -763,26 +763,26 @@
     by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1)
 qed
 
-lemma det_nz_iff_inj:
+lemma%unimportant  det_nz_iff_inj:
   fixes f :: "real^'n \<Rightarrow> real^'n"
   assumes "linear f"
   shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f"
   using det_nz_iff_inj_gen[of f] assms
   unfolding linear_matrix_vector_mul_eq .
 
-lemma det_eq_0_rank:
+lemma%unimportant  det_eq_0_rank:
   fixes A :: "real^'n^'n"
   shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)"
   using invertible_det_nz [of A]
   by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective)
 
-subsubsection\<open>Invertibility of matrices and corresponding linear functions\<close>
+subsubsection%important  \<open>Invertibility of matrices and corresponding linear functions\<close>
 
-lemma matrix_left_invertible_gen:
+lemma%important  matrix_left_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear ( *s) ( *s) f"
   shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id))"
-proof safe
+proof%unimportant safe
   fix B
   assume 1: "B ** matrix f = mat 1"
   show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
@@ -801,12 +801,12 @@
   then show "\<exists>B. B ** matrix f = mat 1" ..
 qed
 
-lemma matrix_left_invertible:
+lemma%unimportant  matrix_left_invertible:
   "linear f \<Longrightarrow> ((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> g \<circ> f = id))" for f::"real^'m \<Rightarrow> real^'n"
   using matrix_left_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma matrix_right_invertible_gen:
+lemma%unimportant  matrix_right_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a^'n"
   assumes "Vector_Spaces.linear ( *s) ( *s) f"
   shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id))"
@@ -829,12 +829,12 @@
   then show "\<exists>B. matrix f ** B = mat 1" ..
 qed
 
-lemma matrix_right_invertible:
+lemma%unimportant  matrix_right_invertible:
   "linear f \<Longrightarrow> ((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id))" for f::"real^'m \<Rightarrow> real^'n"
   using matrix_right_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma matrix_invertible_gen:
+lemma%unimportant  matrix_invertible_gen:
   fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n"
   assumes "Vector_Spaces.linear ( *s) ( *s) f"
   shows  "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
@@ -847,13 +847,13 @@
     by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1)
 qed
 
-lemma matrix_invertible:
+lemma%unimportant  matrix_invertible:
   "linear f \<Longrightarrow> invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)"
   for f::"real^'m \<Rightarrow> real^'n"
   using matrix_invertible_gen[of f]
   by (auto simp: linear_matrix_vector_mul_eq)
 
-lemma invertible_eq_bij:
+lemma%unimportant  invertible_eq_bij:
   fixes m :: "'a::field^'m^'n"
   shows "invertible m \<longleftrightarrow> bij (( *v) m)"
   using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul]
@@ -861,15 +861,15 @@
       vec.linear_injective_left_inverse vec.linear_surjective_right_inverse)
 
 
-subsection \<open>Cramer's rule\<close>
+subsection%important \<open>Cramer's rule\<close>
 
-lemma cramer_lemma_transpose:
+lemma%important  cramer_lemma_transpose:
   fixes A:: "'a::{field}^'n^'n"
     and x :: "'a::{field}^'n"
   shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
                              else row i A)::'a::{field}^'n^'n) = x$k * det A"
   (is "?lhs = ?rhs")
-proof -
+proof%unimportant -
   let ?U = "UNIV :: 'n set"
   let ?Uk = "?U - {k}"
   have U: "?U = insert k ?Uk"
@@ -899,10 +899,10 @@
     done
 qed
 
-lemma cramer_lemma:
+lemma%important  cramer_lemma:
   fixes A :: "'a::{field}^'n^'n"
   shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A"
-proof -
+proof%unimportant -
   let ?U = "UNIV :: 'n set"
   have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
     by (auto intro: sum.cong)
@@ -916,11 +916,11 @@
     done
 qed
 
-lemma cramer:
+lemma%important  cramer:
   fixes A ::"'a::{field}^'n^'n"
   assumes d0: "det A \<noteq> 0"
   shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)"
-proof -
+proof%unimportant -
   from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
     unfolding invertible_det_nz[symmetric] invertible_def
     by blast
@@ -941,14 +941,14 @@
     by auto
 qed
 
-subsection \<open>Orthogonality of a transformation and matrix\<close>
+subsection%important  \<open>Orthogonality of a transformation and matrix\<close>
 
-definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
+definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
 
-definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
+definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
   transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
 
-lemma orthogonal_transformation:
+lemma%unimportant  orthogonal_transformation:
   "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
   unfolding orthogonal_transformation_def
   apply auto
@@ -957,70 +957,70 @@
   apply (simp add: dot_norm linear_add[symmetric])
   done
 
-lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   by (simp add: linear_iff orthogonal_transformation_def)
 
-lemma orthogonal_orthogonal_transformation:
+lemma%unimportant  orthogonal_orthogonal_transformation:
     "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
   by (simp add: orthogonal_def orthogonal_transformation_def)
 
-lemma orthogonal_transformation_compose:
+lemma%unimportant  orthogonal_transformation_compose:
    "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
   by (auto simp: orthogonal_transformation_def linear_compose)
 
-lemma orthogonal_transformation_neg:
+lemma%unimportant  orthogonal_transformation_neg:
   "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
 
-lemma orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
+lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
   by (simp add: linear_iff orthogonal_transformation_def)
 
-lemma orthogonal_transformation_linear:
+lemma%unimportant  orthogonal_transformation_linear:
    "orthogonal_transformation f \<Longrightarrow> linear f"
   by (simp add: orthogonal_transformation_def)
 
-lemma orthogonal_transformation_inj:
+lemma%unimportant  orthogonal_transformation_inj:
   "orthogonal_transformation f \<Longrightarrow> inj f"
   unfolding orthogonal_transformation_def inj_on_def
   by (metis vector_eq)
 
-lemma orthogonal_transformation_surj:
+lemma%unimportant  orthogonal_transformation_surj:
   "orthogonal_transformation f \<Longrightarrow> surj f"
   for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear)
 
-lemma orthogonal_transformation_bij:
+lemma%unimportant  orthogonal_transformation_bij:
   "orthogonal_transformation f \<Longrightarrow> bij f"
   for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj)
 
-lemma orthogonal_transformation_inv:
+lemma%unimportant  orthogonal_transformation_inv:
   "orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)"
   for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
   by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj)
 
-lemma orthogonal_transformation_norm:
+lemma%unimportant  orthogonal_transformation_norm:
   "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   by (metis orthogonal_transformation)
 
-lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
+lemma%unimportant  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
   by (metis matrix_left_right_inverse orthogonal_matrix_def)
 
-lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
+lemma%unimportant  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
   by (simp add: orthogonal_matrix_def)
 
-lemma orthogonal_matrix_mul:
+lemma%unimportant  orthogonal_matrix_mul:
   fixes A :: "real ^'n^'n"
   assumes  "orthogonal_matrix A" "orthogonal_matrix B"
   shows "orthogonal_matrix(A ** B)"
   using assms
   by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
 
-lemma orthogonal_transformation_matrix:
+lemma%important  orthogonal_transformation_matrix:
   fixes f:: "real^'n \<Rightarrow> real^'n"
   shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof -
+proof%unimportant -
   let ?mf = "matrix f"
   let ?ot = "orthogonal_transformation f"
   let ?U = "UNIV :: 'n set"
@@ -1063,11 +1063,11 @@
     by (auto simp: linear_def scalar_mult_eq_scaleR)
 qed
 
-lemma det_orthogonal_matrix:
+lemma%important  det_orthogonal_matrix:
   fixes Q:: "'a::linordered_idom^'n^'n"
   assumes oQ: "orthogonal_matrix Q"
   shows "det Q = 1 \<or> det Q = - 1"
-proof -
+proof%unimportant -
   have "Q ** transpose Q = mat 1"
     by (metis oQ orthogonal_matrix_def)
   then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
@@ -1078,20 +1078,20 @@
     by (simp add: square_eq_1_iff)
 qed
 
-lemma orthogonal_transformation_det [simp]:
+lemma%important  orthogonal_transformation_det [simp]:
   fixes f :: "real^'n \<Rightarrow> real^'n"
   shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1"
-  using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
+  using%unimportant det_orthogonal_matrix orthogonal_transformation_matrix by fastforce
 
 
-subsection \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
+subsection%important  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
 
-lemma scaling_linear:
+lemma%important  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"
   shows "linear f"
-proof -
+proof%unimportant -
   {
     fix v w
     have "norm (f x) = c * norm x" for x
@@ -1105,13 +1105,13 @@
     by (simp add: inner_add field_simps)
 qed
 
-lemma isometry_linear:
+lemma%unimportant  isometry_linear:
   "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
   by (rule scaling_linear[where c=1]) simp_all
 
 text \<open>Hence another formulation of orthogonal transformation\<close>
 
-lemma orthogonal_transformation_isometry:
+lemma%important  orthogonal_transformation_isometry:
   "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
   unfolding orthogonal_transformation
   apply (auto simp: linear_0 isometry_linear)
@@ -1119,7 +1119,7 @@
   by (metis dist_0_norm)
 
 
-lemma image_orthogonal_transformation_ball:
+lemma%unimportant  image_orthogonal_transformation_ball:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes "orthogonal_transformation f"
   shows "f ` ball x r = ball (f x) r"
@@ -1135,7 +1135,7 @@
     by (auto simp: orthogonal_transformation_isometry)
 qed
 
-lemma image_orthogonal_transformation_cball:
+lemma%unimportant  image_orthogonal_transformation_cball:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
   assumes "orthogonal_transformation f"
   shows "f ` cball x r = cball (f x) r"
@@ -1151,31 +1151,31 @@
     by (auto simp: orthogonal_transformation_isometry)
 qed
 
-subsection\<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
+subsection%important \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
 
-lemma orthogonal_matrix_transpose [simp]:
+lemma%unimportant  orthogonal_matrix_transpose [simp]:
      "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
   by (auto simp: orthogonal_matrix_def)
 
-lemma orthogonal_matrix_orthonormal_columns:
+lemma%unimportant  orthogonal_matrix_orthonormal_columns:
   fixes A :: "real^'n^'n"
   shows "orthogonal_matrix A \<longleftrightarrow>
           (\<forall>i. norm(column i A) = 1) \<and>
           (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
   by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
 
-lemma orthogonal_matrix_orthonormal_rows:
+lemma%unimportant  orthogonal_matrix_orthonormal_rows:
   fixes A :: "real^'n^'n"
   shows "orthogonal_matrix A \<longleftrightarrow>
           (\<forall>i. norm(row i A) = 1) \<and>
           (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
   using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
 
-lemma orthogonal_matrix_exists_basis:
+lemma%important  orthogonal_matrix_exists_basis:
   fixes a :: "real^'n"
   assumes "norm a = 1"
   obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
-proof -
+proof%unimportant -
   obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
    and "independent S" "card S = CARD('n)" "span S = UNIV"
     using vector_in_orthonormal_basis assms by force
@@ -1198,11 +1198,11 @@
   qed
 qed
 
-lemma orthogonal_transformation_exists_1:
+lemma%unimportant  orthogonal_transformation_exists_1:
   fixes a b :: "real^'n"
   assumes "norm a = 1" "norm b = 1"
   obtains f where "orthogonal_transformation f" "f a = b"
-proof -
+proof%unimportant -
   obtain k::'n where True
     by simp
   obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
@@ -1220,11 +1220,11 @@
   qed
 qed
 
-lemma orthogonal_transformation_exists:
+lemma%important  orthogonal_transformation_exists:
   fixes a b :: "real^'n"
   assumes "norm a = norm b"
   obtains f where "orthogonal_transformation f" "f a = b"
-proof (cases "a = 0 \<or> b = 0")
+proof%unimportant (cases "a = 0 \<or> b = 0")
   case True
   with assms show ?thesis
     using that by force
@@ -1246,14 +1246,14 @@
 qed
 
 
-subsection \<open>Can extend an isometry from unit sphere\<close>
+subsection%important  \<open>Can extend an isometry from unit sphere\<close>
 
-lemma isometry_sphere_extend:
+lemma%important  isometry_sphere_extend:
   fixes f:: "'a::real_inner \<Rightarrow> 'a"
   assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
     and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
   shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
-proof -
+proof%unimportant -
   {
     fix x y x' y' u v u' v' :: "'a"
     assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
@@ -1286,31 +1286,31 @@
     by (rule exI[where x= ?g]) (metis thfg thd)
 qed
 
-subsection \<open>Rotation, reflection, rotoinversion\<close>
+subsection%important  \<open>Rotation, reflection, rotoinversion\<close>
 
-definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
-definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
+definition%important  "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
+definition%important  "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
 
-lemma orthogonal_rotation_or_rotoinversion:
+lemma%important  orthogonal_rotation_or_rotoinversion:
   fixes Q :: "'a::linordered_idom^'n^'n"
   shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
-  by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
+  by%unimportant (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
 
 text \<open>Explicit formulas for low dimensions\<close>
 
-lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1"
+lemma%unimportant  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
   by simp
 
-lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
+lemma%unimportant  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
 
-lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
+lemma%unimportant  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
 
-lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
+lemma%unimportant  det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
   by (simp add: det_def sign_id)
 
-lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
+lemma%unimportant  det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
 proof -
   have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
   show ?thesis
@@ -1320,7 +1320,7 @@
     by (simp add: sign_swap_id sign_id swap_id_eq)
 qed
 
-lemma det_3:
+lemma%unimportant  det_3:
   "det (A::'a::comm_ring_1^3^3) =
     A$1$1 * A$2$2 * A$3$3 +
     A$1$2 * A$2$3 * A$3$1 +
@@ -1344,7 +1344,7 @@
 
 text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close>
 
-lemma rotation_matrix_exists_basis:
+lemma%unimportant  rotation_matrix_exists_basis:
   fixes a :: "real^'n"
   assumes 2: "2 \<le> CARD('n)" and "norm a = 1"
   obtains A where "rotation_matrix A" "A *v (axis k 1) = a"
@@ -1383,7 +1383,7 @@
   qed
 qed
 
-lemma rotation_exists_1:
+lemma%unimportant  rotation_exists_1:
   fixes a :: "real^'n"
   assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1"
   obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
@@ -1406,7 +1406,7 @@
   qed
 qed
 
-lemma rotation_exists:
+lemma%unimportant  rotation_exists:
   fixes a :: "real^'n"
   assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b"
   obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b"
@@ -1428,7 +1428,7 @@
   with f show thesis ..
 qed
 
-lemma rotation_rightward_line:
+lemma%unimportant  rotation_rightward_line:
   fixes a :: "real^'n"
   obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1"
                   "f(norm a *\<^sub>R axis k 1) = a"