src/HOL/Analysis/Elementary_Metric_Spaces.thy

 
 section \<open>Elementary Metric Spaces\<close>
 
 subsection \<open>Open and closed balls\<close>
 
-definition%important ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition\<^marker>\<open>tag important\<close> ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "ball x e = {y. dist x y < e}"
 
-definition%important cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition\<^marker>\<open>tag important\<close> cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "cball x e = {y. dist x y \<le> e}"
 
-definition%important sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+definition\<^marker>\<open>tag important\<close> sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   where "sphere x e = {y. dist x y = e}"
 
 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   by (simp add: ball_def)
 

 
 
 subsection \<open>Boundedness\<close>
 
   (* FIXME: This has to be unified with BSEQ!! *)
-definition%important (in metric_space) bounded :: "'a set \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> (in metric_space) bounded :: "'a set \<Rightarrow> bool"
   where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
 
 lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
   unfolding bounded_def subset_eq  by auto (meson order_trans zero_le_dist)
 

     using \<open>a \<in> s\<close> by blast
 qed
 
 subsection \<open>The diameter of a set\<close>
 
-definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
+definition\<^marker>\<open>tag important\<close> diameter :: "'a::metric_space set \<Rightarrow> real" where
   "diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"
 
 lemma diameter_empty [simp]: "diameter{} = 0"
   by (auto simp: diameter_def)
 

 lemma compact_closure [simp]:
   fixes S :: "'a::heine_borel set"
   shows "compact(closure S) \<longleftrightarrow> bounded S"
 by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed)
 
-instance%important real :: heine_borel
-proof%unimportant
+instance\<^marker>\<open>tag important\<close> real :: heine_borel
+proof
   fix f :: "nat \<Rightarrow> real"
   assume f: "bounded (range f)"
   obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
     unfolding comp_def by (metis seq_monosub)
   then have "Bseq (f \<circ> r)"

 
 lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
   unfolding bounded_def
   by (metis (no_types, hide_lams) dist_snd_le image_iff order.trans)
 
-instance%important prod :: (heine_borel, heine_borel) heine_borel
-proof%unimportant
+instance\<^marker>\<open>tag important\<close> prod :: (heine_borel, heine_borel) heine_borel
+proof
   fix f :: "nat \<Rightarrow> 'a \<times> 'b"
   assume f: "bounded (range f)"
   then have "bounded (fst ` range f)"
     by (rule bounded_fst)
   then have s1: "bounded (range (fst \<circ> f))"

   shows "\<exists>!x. (f x = x)"
   using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
   by auto
 
 
-subsection%unimportant\<open> Finite intersection property\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open> Finite intersection property\<close>
 
 text\<open>Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\<close>
 
 lemma closed_imp_fip:
   fixes S :: "'a::heine_borel set"

 qed
 
 
 subsection \<open>Infimum Distance\<close>
 
-definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
+definition\<^marker>\<open>tag important\<close> "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
 
 lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
   by (auto intro!: zero_le_dist)
 
 lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"

   using f
     unfolding continuous_on_iff uniformly_continuous_on_def
     by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"])
 
 
-subsection%unimportant\<open> Theorems relating continuity and uniform continuity to closures\<close>
+subsection\<^marker>\<open>tag unimportant\<close>\<open> Theorems relating continuity and uniform continuity to closures\<close>
 
 lemma continuous_on_closure:
    "continuous_on (closure S) f \<longleftrightarrow>
     (\<forall>x e. x \<in> closure S \<and> 0 < e
            \<longrightarrow> (\<exists>d. 0 < d \<and> (\<forall>y. y \<in> S \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e)))"

   with a have "\<Inter>(range S) = {a}"
     unfolding image_def by auto
   then show ?thesis ..
 qed
 
-subsection%unimportant \<open>Making a continuous function avoid some value in a neighbourhood\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Making a continuous function avoid some value in a neighbourhood\<close>
 
 lemma continuous_within_avoid:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::t1_space"
   assumes "continuous (at x within s) f"
     and "f x \<noteq> a"

   by auto
 
 
 subsection\<open>The infimum of the distance between two sets\<close>
 
-definition%important setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+definition\<^marker>\<open>tag important\<close> setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
   "setdist s t \<equiv>
        (if s = {} \<or> t = {} then 0
         else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
 
 lemma setdist_empty1 [simp]: "setdist {} t = 0"