# HG changeset patch
# User nipkow
# Date 1546345597 -3600
# Node ID a59f7d07bf1748638c22533801b27430788c489d
# Parent  8fd576a99a5949839b92ba668abb9da7cb58b943
tuned defs

diff -r 8fd576a99a59 -r a59f7d07bf17 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Mon Dec 31 22:21:34 2018 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 01 13:26:37 2019 +0100
@@ -687,7 +687,8 @@
 
 subsection \<open>Interior of a Set\<close>
 
-definition%important "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+definition%important interior :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
 
 lemma interiorI [intro?]:
   assumes "open T" and "x \<in> T" and "T \<subseteq> S"
@@ -851,7 +852,8 @@
 
 subsection \<open>Closure of a Set\<close>
 
-definition%important "closure S = S \<union> {x | x. x islimpt S}"
+definition%important closure :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"closure S = S \<union> {x . x islimpt S}"
 
 lemma interior_closure: "interior S = - (closure (- S))"
   by (auto simp: interior_def closure_def islimpt_def)
@@ -980,7 +982,8 @@
 
 subsection \<open>Frontier (also known as boundary)\<close>
 
-definition%important "frontier S = closure S - interior S"
+definition%important frontier :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"frontier S = closure S - interior S"
 
 lemma frontier_closed [iff]: "closed (frontier S)"
   by (simp add: frontier_def closed_Diff)
@@ -1630,8 +1633,10 @@
   with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
 qed
 
-definition%important "countably_compact U \<longleftrightarrow>
-    (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
+definition%important countably_compact :: "('a::topological_space) set \<Rightarrow> bool" where
+"countably_compact U \<longleftrightarrow>
+  (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A
+     \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
 
 lemma countably_compactE:
   assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C"
@@ -1698,9 +1703,10 @@
 
 subsubsection\<open>Sequential compactness\<close>
 
-definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool"
-  where "seq_compact S \<longleftrightarrow>
-    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
+definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool" where
+"seq_compact S \<longleftrightarrow>
+  (\<forall>f. (\<forall>n. f n \<in> S)
+    \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
 
 lemma seq_compactI:
   assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
diff -r 8fd576a99a59 -r a59f7d07bf17 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Mon Dec 31 22:21:34 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jan 01 13:26:37 2019 +0100
@@ -1388,7 +1388,8 @@
 subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
 
 definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
-  "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
+"distr M N f =
+  measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
 
 lemma
   shows sets_distr[simp, measurable_cong]: "sets (distr M N f) = sets N"
@@ -1708,9 +1709,8 @@
 
 subsection \<open>Set of measurable sets with finite measure\<close>
 
-definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
-where
-  "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
+definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set" where
+"fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
 
 lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
   by (auto simp: fmeasurable_def)
@@ -2605,7 +2605,8 @@
 
 subsection%unimportant \<open>Null measure\<close>
 
-definition "null_measure M = sigma (space M) (sets M)"
+definition null_measure :: "'a measure \<Rightarrow> 'a measure" where
+"null_measure M = sigma (space M) (sets M)"
 
 lemma space_null_measure[simp]: "space (null_measure M) = space M"
   by (simp add: null_measure_def)
@@ -2626,9 +2627,8 @@
 
 subsection \<open>Scaling a measure\<close>
 
-definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
-  "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
+definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
+"scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
 
 lemma space_scale_measure: "space (scale_measure r M) = space M"
   by (simp add: scale_measure_def)
@@ -2874,9 +2874,10 @@
     by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
   done
 
-definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
-  "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
+"sup_measure' A B =
+  measure_of (space A) (sets A)
+    (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
 
 lemma assumes [simp]: "sets B = sets A"
   shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A"
@@ -3002,10 +3003,11 @@
   qed
 qed simp_all
 
-definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-where
-  "sup_lexord A B k s c =
-    (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
+definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+"sup_lexord A B k s c =
+  (if k A = k B then c else
+   if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else
+   if k B \<le> k A then A else B)"
 
 lemma sup_lexord:
   "(k A < k B \<Longrightarrow> P B) \<Longrightarrow> (k B < k A \<Longrightarrow> P A) \<Longrightarrow> (k A = k B \<Longrightarrow> P c) \<Longrightarrow>
@@ -3031,8 +3033,7 @@
 instantiation measure :: (type) semilattice_sup
 begin
 
-definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
+definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
   "sup_measure A B =
     sup_lexord A B space (sigma (space A \<union> space B) {})
       (sup_lexord A B sets (sigma (space A) (sets A \<union> sets B)) (sup_measure' A B))"
@@ -3135,9 +3136,12 @@
 lemma UN_space_closed: "\<Union>(sets ` S) \<subseteq> Pow (\<Union>(space ` S))"
   using sets.space_closed by auto
 
-definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
+definition%important
+  Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
 where
-  "Sup_lexord k c s A = (let U = (SUP a\<in>A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
+  "Sup_lexord k c s A =
+  (let U = (SUP a\<in>A. k a)
+   in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
 
 lemma Sup_lexord:
   "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a\<in>A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a\<in>A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
@@ -3194,9 +3198,9 @@
   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
   by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
 
-definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
-where
-  "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
+definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure" where
+"Sup_measure' M =
+  measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
     (\<lambda>X. (SUP P\<in>{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
 
 lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
@@ -3265,21 +3269,20 @@
     using assms * by auto
 qed (rule UN_space_closed)
 
-definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
-where
-  "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
-    (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
-
-definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
-where
+definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure" where
+"Sup_measure =
+  Sup_lexord space
+    (Sup_lexord sets Sup_measure'
+      (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u)))
+    (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
+
+definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure" where
   "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
 
-definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
+definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
   "inf_measure a b = Inf {a, b}"
 
-definition%important top_measure :: "'a measure"
-where
+definition%important top_measure :: "'a measure" where
   "top_measure = Inf {}"
 
 instance