# HG changeset patch
# User haftmann
# Date 1470848240 -7200
# Node ID 7faa9bf9860bd42525964a90e2aef4677e84113f
# Parent  3663157ee197166259b28ef74d82fe091d0b9f1b
epheremal interpretation keeps auxiliary definition localized

diff -r 3663157ee197 -r 7faa9bf9860b src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Aug 10 18:57:20 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Aug 10 18:57:20 2016 +0200
@@ -2641,8 +2641,11 @@
     by (simp add: A(3))
 qed
 
+instantiation measure :: (type) complete_lattice
+begin
+
 interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
-  proof qed (auto intro!: antisym)
+  by standard (auto intro!: antisym)
 
 lemma sup_measure_F_mono':
   "finite J \<Longrightarrow> finite I \<Longrightarrow> sup_measure.F id I \<le> sup_measure.F id (I \<union> J)"
@@ -2744,9 +2747,6 @@
     using assms * by auto
 qed (rule UN_space_closed)
 
-instantiation measure :: (type) complete_lattice
-begin
-
 definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
 where
   "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
@@ -2947,11 +2947,12 @@
   assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N" "I \<noteq> {}"
   shows "emeasure (SUP i:I. M i) X = (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i:J. M i) X)"
 proof -
+  interpret sup_measure: comm_monoid_set sup "bot :: 'b measure"
+    by standard (auto intro!: antisym)
   have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i:J. i)" for J :: "'b measure set"
     by (induction J rule: finite_induct) auto
   have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x:J. M x) = sets N" for J
     by (intro sets_SUP sets) (auto )
-
   from \<open>I \<noteq> {}\<close> obtain i where "i\<in>I" by auto
   have "Sup_measure' (M`I) X = (SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
     using sets by (intro emeasure_Sup_measure') auto
@@ -3308,7 +3309,7 @@
     note singleton_sets = this
     have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
       using \<open>?M \<noteq> 0\<close>
-      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
+      by (simp add: \<open>card X = Suc (Suc n)\<close> field_simps less_le)
     also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
       by (rule setsum_mono) fact
     also have "\<dots> = measure M (\<Union>x\<in>X. {x})"