src/HOL/Analysis/Linear_Algebra.thy

     then have "x \<in> ((\<lambda>x. a+x) ` S)" by auto
   }
   then show ?thesis by auto
 qed
 
-subsection%unimportant \<open>More interesting properties of the norm\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>More interesting properties of the norm\<close>
 
 unbundle inner_syntax
 
 text\<open>Equality of vectors in terms of \<^term>\<open>(\<bullet>)\<close> products.\<close>
 

 qed simp
 
 
 subsection \<open>Orthogonality\<close>
 
-definition%important (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
+definition\<^marker>\<open>tag important\<close> (in real_inner) "orthogonal x y \<longleftrightarrow> x \<bullet> y = 0"
 
 context real_inner
 begin
 
 lemma orthogonal_self: "orthogonal x x \<longleftrightarrow> x = 0"

 qed
 
 
 subsection  \<open>Orthogonality of a transformation\<close>
 
-definition%important  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
-
-lemma%unimportant  orthogonal_transformation:
+definition\<^marker>\<open>tag important\<close>  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
+
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation:
   "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)"
   unfolding orthogonal_transformation_def
   apply auto
   apply (erule_tac x=v in allE)+
   apply (simp add: norm_eq_sqrt_inner)
   apply (simp add: dot_norm linear_add[symmetric])
   done
 
-lemma%unimportant  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)"
   by (simp add: linear_iff orthogonal_transformation_def)
 
-lemma%unimportant  orthogonal_orthogonal_transformation:
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_compose:
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_neg:
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_neg:
   "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
 
-lemma%unimportant  orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v"
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_linear:
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_linear:
    "orthogonal_transformation f \<Longrightarrow> linear f"
   by (simp add: orthogonal_transformation_def)
 
-lemma%unimportant  orthogonal_transformation_inj:
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_inj:
   "orthogonal_transformation f \<Longrightarrow> inj f"
   unfolding orthogonal_transformation_def inj_on_def
   by (metis vector_eq)
 
-lemma%unimportant  orthogonal_transformation_surj:
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_bij:
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_inv:
+lemma\<^marker>\<open>tag unimportant\<close>  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%unimportant  orthogonal_transformation_norm:
+lemma\<^marker>\<open>tag unimportant\<close>  orthogonal_transformation_norm:
   "orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x"
   by (metis orthogonal_transformation)
 
 
 subsection \<open>Bilinear functions\<close>
 
-definition%important
+definition\<^marker>\<open>tag important\<close>
 bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
 "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
 
 lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
   by (simp add: bilinear_def linear_iff)

 qed
 
 
 subsection \<open>Adjoints\<close>
 
-definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
+definition\<^marker>\<open>tag important\<close> adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
 "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
 
 lemma adjoint_unique:
   assumes "\<forall>x y. inner (f x) y = inner x (g y)"
   shows "adjoint f = g"

   apply auto
   apply (metis Suc_pred of_nat_Suc)
   done
 
 
-subsection%unimportant \<open>Euclidean Spaces as Typeclass\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Euclidean Spaces as Typeclass\<close>
 
 lemma independent_Basis: "independent Basis"
   by (rule independent_Basis)
 
 lemma span_Basis [simp]: "span Basis = UNIV"

 
 lemma in_span_Basis: "x \<in> span Basis"
   unfolding span_Basis ..
 
 
-subsection%unimportant \<open>Linearity and Bilinearity continued\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Linearity and Bilinearity continued\<close>
 
 lemma linear_bounded:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"
   shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"

   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   shows "linear f \<Longrightarrow> f differentiable net"
   by (metis linear_imp_has_derivative differentiable_def)
 
 
-subsection%unimportant \<open>We continue\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>We continue\<close>
 
 lemma independent_bound:
   fixes S :: "'a::euclidean_space set"
   shows "independent S \<Longrightarrow> finite S \<and> card S \<le> DIM('a)"
   by (metis dim_subset_UNIV finiteI_independent dim_span_eq_card_independent)

   using bilinear_eq[OF bf bg equalityD2[OF span_Basis] equalityD2[OF span_Basis]] fg by blast
 
 
 subsection \<open>Infinity norm\<close>
 
-definition%important "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
+definition\<^marker>\<open>tag important\<close> "infnorm (x::'a::euclidean_space) = Sup {\<bar>x \<bullet> b\<bar> |b. b \<in> Basis}"
 
 lemma infnorm_set_image:
   fixes x :: "'a::euclidean_space"
   shows "{\<bar>x \<bullet> i\<bar> |i. i \<in> Basis} = (\<lambda>i. \<bar>x \<bullet> i\<bar>) ` Basis"
   by blast

 qed
 
 
 subsection \<open>Collinearity\<close>
 
-definition%important collinear :: "'a::real_vector set \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> collinear :: "'a::real_vector set \<Rightarrow> bool"
   where "collinear S \<longleftrightarrow> (\<exists>u. \<forall>x \<in> S. \<forall> y \<in> S. \<exists>c. x - y = c *\<^sub>R u)"
 
 lemma collinear_alt:
      "collinear S \<longleftrightarrow> (\<exists>u v. \<forall>x \<in> S. \<exists>c. x = u + c *\<^sub>R v)" (is "?lhs = ?rhs")
 proof

     using assms pairwise_orthogonal_imp_finite by auto
   with \<open>span B = span T\<close> show ?thesis
     by (rule_tac U=U in that) (auto simp: span_Un)
 qed
 
-corollary%unimportant orthogonal_extension_strong:
+corollary\<^marker>\<open>tag unimportant\<close> orthogonal_extension_strong:
   fixes S :: "'a::euclidean_space set"
   assumes S: "pairwise orthogonal S"
   obtains U where "U \<inter> (insert 0 S) = {}" "pairwise orthogonal (S \<union> U)"
                   "span (S \<union> U) = span (S \<union> T)"
 proof -

   show ?thesis
     by (rule that [OF 1 2 3 4 5 6])
 qed
 
 
-proposition%unimportant orthogonal_to_subspace_exists_gen:
+proposition\<^marker>\<open>tag unimportant\<close> orthogonal_to_subspace_exists_gen:
   fixes S :: "'a :: euclidean_space set"
   assumes "span S \<subset> span T"
   obtains x where "x \<noteq> 0" "x \<in> span T" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
 proof -
   obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"

     ultimately show ?thesis
       using \<open>x \<noteq> 0\<close> that \<open>span B = span S\<close> by auto
   qed
 qed
 
-corollary%unimportant orthogonal_to_subspace_exists:
+corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_subspace_exists:
   fixes S :: "'a :: euclidean_space set"
   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"

       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)
 qed
 
-corollary%unimportant orthogonal_to_vector_exists:
+corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_vector_exists:
   fixes x :: "'a :: euclidean_space"
   assumes "2 \<le> DIM('a)"
   obtains y where "y \<noteq> 0" "orthogonal x y"
 proof -
   have "dim {x} < DIM('a)"
     using assms by auto
   then show thesis
     by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
 qed
 
-proposition%unimportant orthogonal_subspace_decomp_exists:
+proposition\<^marker>\<open>tag unimportant\<close> orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z
   where "y \<in> span S"
     and "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w"
     and "x = y + z"