tuned order of declarations and proofs
authorhaftmann
Wed Aug 10 18:57:20 2016 +0200 (2016-08-10)
changeset 636573663157ee197
parent 63656 fac9097dc772
child 63658 7faa9bf9860b
tuned order of declarations and proofs
src/HOL/Analysis/Measure_Space.thy
     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.6  
     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.51  
    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.55  
    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.65  
    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.79  
    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.85  
    1.86 @@ -2720,30 +2744,6 @@
    1.87      using assms * by auto
    1.88  qed (rule UN_space_closed)
    1.89  
    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.113 -
   1.114  instantiation measure :: (type) complete_lattice
   1.115  begin
   1.116