src/HOL/Analysis/Tagged_Division.thy

 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff
   scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one
 
 
-subsection%unimportant \<open>Sundries\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Sundries\<close>
 
 
 text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
 lemma wf_finite_segments:
   assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"

 lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
   by (simp add: box_ne_empty)
 
 subsection \<open>Bounds on intervals where they exist\<close>
 
-definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
+definition\<^marker>\<open>tag important\<close> interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
 
-definition%important interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
+definition\<^marker>\<open>tag important\<close> interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x\<in>s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
     interval_upperbound (cbox a b) = (b::'a::euclidean_space)"

       by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
 qed
 
 subsection \<open>The notion of a gauge --- simply an open set containing the point\<close>
 
-definition%important "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
+definition\<^marker>\<open>tag important\<close> "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
 
 lemma gaugeI:
   assumes "\<And>x. x \<in> \<gamma> x"
     and "\<And>x. open (\<gamma> x)"
   shows "gauge \<gamma>"

   shows "gauge (\<lambda>x. {y. f y \<in> d (f x)})"
   using assms unfolding gauge_def by force
 
 subsection \<open>Divisions\<close>
 
-definition%important division_of (infixl "division'_of" 40)
+definition\<^marker>\<open>tag important\<close> division_of (infixl "division'_of" 40)
 where
   "s division_of i \<longleftrightarrow>
     finite s \<and>
     (\<forall>K\<in>s. K \<subseteq> i \<and> K \<noteq> {} \<and> (\<exists>a b. K = cbox a b)) \<and>
     (\<forall>K1\<in>s. \<forall>K2\<in>s. K1 \<noteq> K2 \<longrightarrow> interior(K1) \<inter> interior(K2) = {}) \<and>

   }
 qed
 
 subsection \<open>Tagged (partial) divisions\<close>
 
-definition%important tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
+definition\<^marker>\<open>tag important\<close> tagged_partial_division_of (infixr "tagged'_partial'_division'_of" 40)
   where "s tagged_partial_division_of i \<longleftrightarrow>
     finite s \<and>
     (\<forall>x K. (x, K) \<in> s \<longrightarrow> x \<in> K \<and> K \<subseteq> i \<and> (\<exists>a b. K = cbox a b)) \<and>
     (\<forall>x1 K1 x2 K2. (x1, K1) \<in> s \<and> (x2, K2) \<in> s \<and> (x1, K1) \<noteq> (x2, K2) \<longrightarrow>
       interior K1 \<inter> interior K2 = {})"

     and "\<And>x K. (x,K) \<in> s \<Longrightarrow> \<exists>a b. K = cbox a b"
     and "\<And>x1 K1 x2 K2. (x1,K1) \<in> s \<Longrightarrow>
       (x2, K2) \<in> s \<Longrightarrow> (x1, K1) \<noteq> (x2, K2) \<Longrightarrow> interior K1 \<inter> interior K2 = {}"
   using assms unfolding tagged_partial_division_of_def by blast+
 
-definition%important tagged_division_of (infixr "tagged'_division'_of" 40)
+definition\<^marker>\<open>tag important\<close> tagged_division_of (infixr "tagged'_division'_of" 40)
   where "s tagged_division_of i \<longleftrightarrow> s tagged_partial_division_of i \<and> (\<Union>{K. \<exists>x. (x,K) \<in> s} = i)"
 
 lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
 

 
 text \<open>This auxiliary structure is used to sum up over the elements of a division. Main theorem is
   \<open>operative_division\<close>. Instances for the monoid are \<^typ>\<open>'a option\<close>, \<^typ>\<open>real\<close>, and
   \<^typ>\<open>bool\<close>.\<close>
 
-paragraph%important \<open>Using additivity of lifted function to encode definedness.\<close>
+paragraph\<^marker>\<open>tag important\<close> \<open>Using additivity of lifted function to encode definedness.\<close>
 text \<open>%whitespace\<close>
-definition%important lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
+definition\<^marker>\<open>tag important\<close> lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
 where
   "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
 
 lemma lift_option_simps[simp]:
   "lift_option f (Some a) (Some b) = Some (f a b)"
   "lift_option f None b' = None"
   "lift_option f a' None = None"
   by (auto simp: lift_option_def)
 
-lemma%important comm_monoid_lift_option:
+lemma\<^marker>\<open>tag important\<close> comm_monoid_lift_option:
   assumes "comm_monoid f z"
   shows "comm_monoid (lift_option f) (Some z)"
 proof -
   from assms interpret comm_monoid f z .
   show ?thesis

   by (meson zero_less_one)
 
 
 paragraph \<open>Division points\<close>
 text \<open>%whitespace\<close>
-definition%important "division_points (k::('a::euclidean_space) set) d =
+definition\<^marker>\<open>tag important\<close> "division_points (k::('a::euclidean_space) set) d =
    {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
      (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"
 
 lemma division_points_finite:
   fixes i :: "'a::euclidean_space set"

 qed
 
 
 subsection \<open>Fine-ness of a partition w.r.t. a gauge\<close>
 
-definition%important fine  (infixr "fine" 46)
+definition\<^marker>\<open>tag important\<close> fine  (infixr "fine" 46)
   where "d fine s \<longleftrightarrow> (\<forall>(x,k) \<in> s. k \<subseteq> d x)"
 
 lemma fineI:
   assumes "\<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x"
   shows "d fine s"

     using assms(1) assms(3) assms(4) pfn(1) tagged_division_Union apply force
     by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
 qed
 (* FIXME structure here, do not have one lemma in each subsection *)
 
-subsection%unimportant \<open>The set we're concerned with must be closed\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>The set we're concerned with must be closed\<close>
 
 lemma division_of_closed:
   fixes i :: "'n::euclidean_space set"
   shows "s division_of i \<Longrightarrow> closed i"
   unfolding division_of_def by fastforce

   with p obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
     by (meson \<open>gauge d\<close>)
   with ptag that show ?thesis by auto
 qed
 
-subsubsection%important \<open>Covering lemma\<close>
+subsubsection\<^marker>\<open>tag important\<close> \<open>Covering lemma\<close>
 
 text\<open> Some technical lemmas used in the approximation results that follow. Proof of the covering
   lemma is an obvious multidimensional generalization of Lemma 3, p65 of Swartz's
   "Introduction to Gauge Integrals". \<close>
 

 
 subsection \<open>Division filter\<close>
 
 text \<open>Divisions over all gauges towards finer divisions.\<close>
 
-definition%important division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
+definition\<^marker>\<open>tag important\<close> division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
   where "division_filter s = (INF g\<in>{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
 
 proposition eventually_division_filter:
   "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
     (\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"