author haftmann Wed Aug 10 18:57:20 2016 +0200 (2016-08-10) changeset 63657 3663157ee197 parent 63656 fac9097dc772 child 63658 7faa9bf9860b
tuned order of declarations and proofs
1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Aug 11 07:36:58 2016 +0200
1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Wed Aug 10 18:57:20 2016 +0200
1.3 @@ -2599,6 +2599,48 @@
1.4  lemma space_empty_eq_bot: "space a = {} \<longleftrightarrow> a = bot"
1.5    using space_empty[of a] by (auto intro!: measure_eqI)
1.7 +lemma sets_eq_iff_bounded: "A \<le> B \<Longrightarrow> B \<le> C \<Longrightarrow> sets A = sets C \<Longrightarrow> sets B = sets A"
1.8 +  by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm)
1.9 +
1.10 +lemma sets_sup: "sets A = sets M \<Longrightarrow> sets B = sets M \<Longrightarrow> sets (sup A B) = sets M"
1.11 +  by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq)
1.12 +
1.13 +lemma le_measureD1: "A \<le> B \<Longrightarrow> space A \<le> space B"
1.14 +  by (auto simp: le_measure_iff split: if_split_asm)
1.15 +
1.16 +lemma le_measureD2: "A \<le> B \<Longrightarrow> space A = space B \<Longrightarrow> sets A \<le> sets B"
1.17 +  by (auto simp: le_measure_iff split: if_split_asm)
1.18 +
1.19 +lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
1.20 +  by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
1.21 +
1.22 +lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
1.23 +  using sets.space_closed by auto
1.24 +
1.25 +definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
1.26 +where
1.27 +  "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)"
1.28 +
1.29 +lemma Sup_lexord:
1.30 +  "(\<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>
1.31 +    P (Sup_lexord k c s A)"
1.32 +  by (auto simp: Sup_lexord_def Let_def)
1.33 +
1.34 +lemma Sup_lexord1:
1.35 +  assumes A: "A \<noteq> {}" "(\<And>a. a \<in> A \<Longrightarrow> k a = (\<Union>a\<in>A. k a))" "P (c A)"
1.36 +  shows "P (Sup_lexord k c s A)"
1.37 +  unfolding Sup_lexord_def Let_def
1.38 +proof (clarsimp, safe)
1.39 +  show "\<forall>a\<in>A. k a \<noteq> (\<Union>x\<in>A. k x) \<Longrightarrow> P (s A)"
1.40 +    by (metis assms(1,2) ex_in_conv)
1.41 +next
1.42 +  fix a assume "a \<in> A" "k a = (\<Union>x\<in>A. k x)"
1.43 +  then have "{a \<in> A. k a = (\<Union>x\<in>A. k x)} = {a \<in> A. k a = k a}"
1.44 +    by (metis A(2)[symmetric])
1.45 +  then show "P (c {a \<in> A. k a = (\<Union>x\<in>A. k x)})"
1.46 +    by (simp add: A(3))
1.47 +qed
1.48 +
1.49  interpretation sup_measure: comm_monoid_set sup "bot :: 'a measure"
1.50    proof qed (auto intro!: antisym)
1.52 @@ -2627,33 +2669,15 @@
1.53  lemma sup_measure_F_mono: "finite I \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sup_measure.F id J \<le> sup_measure.F id I"
1.54    using sup_measure_F_mono'[of I J] by (auto simp: finite_subset Un_absorb1)
1.56 -lemma sets_eq_iff_bounded: "A \<le> B \<Longrightarrow> B \<le> C \<Longrightarrow> sets A = sets C \<Longrightarrow> sets B = sets A"
1.57 -  by (auto dest: sets_eq_imp_space_eq simp add: le_measure_iff split: if_split_asm)
1.58 -
1.59 -lemma sets_sup: "sets A = sets M \<Longrightarrow> sets B = sets M \<Longrightarrow> sets (sup A B) = sets M"
1.60 -  by (auto simp add: sup_measure_def sup_lexord_def dest: sets_eq_imp_space_eq)
1.61 -
1.62  lemma sets_sup_measure_F:
1.63    "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"
1.64    by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
1.66 -lemma le_measureD1: "A \<le> B \<Longrightarrow> space A \<le> space B"
1.67 -  by (auto simp: le_measure_iff split: if_split_asm)
1.68 -
1.69 -lemma le_measureD2: "A \<le> B \<Longrightarrow> space A = space B \<Longrightarrow> sets A \<le> sets B"
1.70 -  by (auto simp: le_measure_iff split: if_split_asm)
1.71 -
1.72 -lemma le_measureD3: "A \<le> B \<Longrightarrow> sets A = sets B \<Longrightarrow> emeasure A X \<le> emeasure B X"
1.73 -  by (auto simp: le_measure_iff le_fun_def dest: sets_eq_imp_space_eq split: if_split_asm)
1.74 -
1.75  definition Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
1.76  where
1.77    "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
1.78      (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
1.80 -lemma UN_space_closed: "UNION S sets \<subseteq> Pow (UNION S space)"
1.81 -  using sets.space_closed by auto
1.82 -
1.83  lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
1.84    unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed])
1.86 @@ -2720,30 +2744,6 @@
1.87      using assms * by auto
1.88  qed (rule UN_space_closed)
1.90 -definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
1.91 -where
1.92 -  "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)"
1.93 -
1.94 -lemma Sup_lexord:
1.95 -  "(\<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>
1.96 -    P (Sup_lexord k c s A)"
1.97 -  by (auto simp: Sup_lexord_def Let_def)
1.98 -
1.99 -lemma Sup_lexord1:
1.100 -  assumes A: "A \<noteq> {}" "(\<And>a. a \<in> A \<Longrightarrow> k a = (\<Union>a\<in>A. k a))" "P (c A)"
1.101 -  shows "P (Sup_lexord k c s A)"
1.102 -  unfolding Sup_lexord_def Let_def
1.103 -proof (clarsimp, safe)
1.104 -  show "\<forall>a\<in>A. k a \<noteq> (\<Union>x\<in>A. k x) \<Longrightarrow> P (s A)"
1.105 -    by (metis assms(1,2) ex_in_conv)
1.106 -next
1.107 -  fix a assume "a \<in> A" "k a = (\<Union>x\<in>A. k x)"
1.108 -  then have "{a \<in> A. k a = (\<Union>x\<in>A. k x)} = {a \<in> A. k a = k a}"
1.109 -    by (metis A(2)[symmetric])
1.110 -  then show "P (c {a \<in> A. k a = (\<Union>x\<in>A. k x)})"
1.111 -    by (simp add: A(3))
1.112 -qed
1.114  instantiation measure :: (type) complete_lattice
1.115  begin