# HG changeset patch
# User haftmann
# Date 1470848240 -7200
# Node ID 3663157ee197166259b28ef74d82fe091d0b9f1b
# Parent  fac9097dc772ecde95c236328f4cc17d2de41db2
tuned order of declarations and proofs

diff -r fac9097dc772 -r 3663157ee197 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Aug 11 07:36:58 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Aug 10 18:57:20 2016 +0200
@@ -2599,6 +2599,48 @@
 lemma space_empty_eq_bot: "space a = {} \<longleftrightarrow> a = bot"
   using space_empty[of a] by (auto intro!: measure_eqI)
 
+lemma sets_eq_iff_bounded: "A \<le> B \<Longrightarrow> B \<le> C \<Longrightarrow> sets A = sets C \<Longrightarrow> sets B = sets A"
+  by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm)
+
+lemma sets_sup: "sets A = sets M \<Longrightarrow> sets B = sets M \<Longrightarrow> sets (sup A B) = sets M"
+  by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq)
+
+lemma le_measureD1: "A \<le> B \<Longrightarrow> space A \<le> space B"
+  by (auto simp: le_measure_iff split: if_split_asm)
+
+lemma le_measureD2: "A \<le> B \<Longrightarrow> space A = space B \<Longrightarrow> sets A \<le> sets B"
+  by (auto simp: le_measure_iff split: if_split_asm)
+
+lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
+  by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
+
+lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
+  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"
+where
+  "Sup_lexord k c s A = (let U = (SUP a: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: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:A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
+    P (Sup_lexord k c s A)"
+  by (auto simp: Sup_lexord_def Let_def)
+
+lemma Sup_lexord1:
+  assumes A: "A \<noteq> {}" "(\<And>a. a \<in> A \<Longrightarrow> k a = (\<Union>a\<in>A. k a))" "P (c A)"
+  shows "P (Sup_lexord k c s A)"
+  unfolding Sup_lexord_def Let_def
+proof (clarsimp, safe)
+  show "\<forall>a\<in>A. k a \<noteq> (\<Union>x\<in>A. k x) \<Longrightarrow> P (s A)"
+    by (metis assms(1,2) ex_in_conv)
+next
+  fix a assume "a \<in> A" "k a = (\<Union>x\<in>A. k x)"
+  then have "{a \<in> A. k a = (\<Union>x\<in>A. k x)} = {a \<in> A. k a = k a}"
+    by (metis A(2)[symmetric])
+  then show "P (c {a \<in> A. k a = (\<Union>x\<in>A. k x)})"
+    by (simp add: A(3))
+qed
+
 interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
   proof qed (auto intro!: antisym)
 
@@ -2627,33 +2669,15 @@
 lemma sup_measure_F_mono: "finite I \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sup_measure.F id J \<le> sup_measure.F id I"
   using sup_measure_F_mono'[of I J] by (auto simp: finite_subset Un_absorb1)
 
-lemma sets_eq_iff_bounded: "A \<le> B \<Longrightarrow> B \<le> C \<Longrightarrow> sets A = sets C \<Longrightarrow> sets B = sets A"
-  by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm)
-
-lemma sets_sup: "sets A = sets M \<Longrightarrow> sets B = sets M \<Longrightarrow> sets (sup A B) = sets M"
-  by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq)
-
 lemma sets_sup_measure_F:
   "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)
 
-lemma le_measureD1: "A \<le> B \<Longrightarrow> space A \<le> space B"
-  by (auto simp: le_measure_iff split: if_split_asm)
-
-lemma le_measureD2: "A \<le> B \<Longrightarrow> space A = space B \<Longrightarrow> sets A \<le> sets B"
-  by (auto simp: le_measure_iff split: if_split_asm)
-
-lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
-  by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
-
 definition 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:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
 
-lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
-  using sets.space_closed by auto
-
 lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
   unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed])
 
@@ -2720,30 +2744,6 @@
     using assms * by auto
 qed (rule UN_space_closed)
 
-definition 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: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: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:A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
-    P (Sup_lexord k c s A)"
-  by (auto simp: Sup_lexord_def Let_def)
-
-lemma Sup_lexord1:
-  assumes A: "A \<noteq> {}" "(\<And>a. a \<in> A \<Longrightarrow> k a = (\<Union>a\<in>A. k a))" "P (c A)"
-  shows "P (Sup_lexord k c s A)"
-  unfolding Sup_lexord_def Let_def
-proof (clarsimp, safe)
-  show "\<forall>a\<in>A. k a \<noteq> (\<Union>x\<in>A. k x) \<Longrightarrow> P (s A)"
-    by (metis assms(1,2) ex_in_conv)
-next
-  fix a assume "a \<in> A" "k a = (\<Union>x\<in>A. k x)"
-  then have "{a \<in> A. k a = (\<Union>x\<in>A. k x)} = {a \<in> A. k a = k a}"
-    by (metis A(2)[symmetric])
-  then show "P (c {a \<in> A. k a = (\<Union>x\<in>A. k x)})"
-    by (simp add: A(3))
-qed
-
 instantiation measure :: (type) complete_lattice
 begin