tidying up including contributions from Paulo Emílio de Vilhena
authorpaulson <lp15@cam.ac.uk>
Wed Apr 18 15:57:36 2018 +0100 (14 months ago)
changeset 679991b05f74f2e5f
parent 67998 73a5a33486ee
child 68000 40b790c5a11d
tidying up including contributions from Paulo Emílio de Vilhena
NEWS
src/HOL/Algebra/Congruence.thy
src/HOL/Analysis/Change_Of_Vars.thy
src/HOL/Analysis/Lebesgue_Measure.thy
     1.1 --- a/NEWS	Tue Apr 17 22:35:48 2018 +0100
     1.2 +++ b/NEWS	Wed Apr 18 15:57:36 2018 +0100
     1.3 @@ -209,6 +209,10 @@
     1.4  choice operator. The dual of this property is also proved in 
     1.5  Hilbert_Choice.thy.
     1.6  
     1.7 +* New syntax for the minimum/maximum of a function over a finite set:
     1.8 +MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
     1.9 +MAX.
    1.10 +
    1.11  * Clarifed theorem names:
    1.12  
    1.13    Min.antimono ~> Min.subset_imp
    1.14 @@ -255,8 +259,9 @@
    1.15  
    1.16  * HOL-Algebra: renamed (^) to [^]
    1.17  
    1.18 -* Session HOL-Analysis: Moebius functions and the Riemann mapping
    1.19 -theorem.
    1.20 +* Session HOL-Analysis: Moebius functions, the Riemann mapping
    1.21 +theorem, the Vitali covering theorem, change-of-variables results for
    1.22 +integration and measures.
    1.23  
    1.24  * Class linordered_semiring_1 covers zero_less_one also, ruling out
    1.25  pathologic instances. Minor INCOMPATIBILITY.
     2.1 --- a/src/HOL/Algebra/Congruence.thy	Tue Apr 17 22:35:48 2018 +0100
     2.2 +++ b/src/HOL/Algebra/Congruence.thy	Wed Apr 18 15:57:36 2018 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4  (*  Title:      HOL/Algebra/Congruence.thy
     2.5      Author:     Clemens Ballarin, started 3 January 2008
     2.6 -    Copyright:  Clemens Ballarin
     2.7 +    with thanks to Paulo Emílio de Vilhena
     2.8  *)
     2.9  
    2.10  theory Congruence
    2.11 @@ -119,7 +119,7 @@
    2.12  by (fast intro: elemI elim: elemE dest: subsetD)
    2.13  
    2.14  lemma (in equivalence) mem_imp_elem [simp, intro]:
    2.15 -  "[| x \<in> A; x \<in> carrier S |] ==> x .\<in> A"
    2.16 +  "\<lbrakk> x \<in> A; x \<in> carrier S \<rbrakk> \<Longrightarrow> x .\<in> A"
    2.17    unfolding elem_def by blast
    2.18  
    2.19  lemma set_eqI:
    2.20 @@ -215,15 +215,11 @@
    2.21  
    2.22  lemma (in equivalence) set_eq_sym [sym]:
    2.23    assumes "A {.=} B"
    2.24 -    and "A \<subseteq> carrier S" "B \<subseteq> carrier S"
    2.25    shows "B {.=} A"
    2.26  using assms
    2.27  unfolding set_eq_def elem_def
    2.28  by fast
    2.29  
    2.30 -(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *)
    2.31 -(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *)
    2.32 -
    2.33  lemma (in equivalence) equal_set_eq_trans [trans]:
    2.34    assumes AB: "A = B" and BC: "B {.=} C"
    2.35    shows "A {.=} C"
    2.36 @@ -234,7 +230,6 @@
    2.37    shows "A {.=} C"
    2.38    using AB BC by simp
    2.39  
    2.40 -
    2.41  lemma (in equivalence) set_eq_trans [trans]:
    2.42    assumes AB: "A {.=} B" and BC: "B {.=} C"
    2.43      and carr: "A \<subseteq> carrier S"  "B \<subseteq> carrier S"  "C \<subseteq> carrier S"
    2.44 @@ -265,46 +260,46 @@
    2.45         show "c .\<in> A" by simp
    2.46  qed
    2.47  
    2.48 -(* FIXME: generalise for insert *)
    2.49 +lemma (in equivalence) set_eq_insert_aux:
    2.50 +  assumes x: "x .= x'"
    2.51 +      and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
    2.52 +    shows "\<forall>a \<in> (insert x A). a .\<in> (insert x' A)"
    2.53 +proof
    2.54 +  fix a
    2.55 +  show "a \<in> insert x A \<Longrightarrow> a .\<in> insert x' A"
    2.56 +  proof cases
    2.57 +    assume "a \<in> A"
    2.58 +    thus "a .\<in> insert x' A"
    2.59 +      using carr(3) by blast
    2.60 +  next
    2.61 +    assume "a \<in> insert x A" "a \<notin> A"
    2.62 +    hence "a = x"
    2.63 +      by blast
    2.64 +    thus "a .\<in> insert x' A"
    2.65 +      by (meson x elemI insertI1)
    2.66 +  qed
    2.67 +qed
    2.68  
    2.69 -(*
    2.70  lemma (in equivalence) set_eq_insert:
    2.71    assumes x: "x .= x'"
    2.72 -    and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
    2.73 -  shows "insert x A {.=} insert x' A"
    2.74 -  unfolding set_eq_def elem_def
    2.75 -apply rule
    2.76 -apply rule
    2.77 -apply (case_tac "xa = x")
    2.78 -using x apply fast
    2.79 -apply (subgoal_tac "xa \<in> A") prefer 2 apply fast
    2.80 -apply (rule_tac x=xa in bexI)
    2.81 -using carr apply (rule_tac refl) apply auto [1]
    2.82 -apply safe
    2.83 -*)
    2.84 +      and carr: "x \<in> carrier S" "x' \<in> carrier S" "A \<subseteq> carrier S"
    2.85 +    shows "insert x A {.=} insert x' A"
    2.86 +proof-
    2.87 +  have "(\<forall>a \<in> (insert x  A). a .\<in> (insert x' A)) \<and>
    2.88 +        (\<forall>a \<in> (insert x' A). a .\<in> (insert x  A))"
    2.89 +    using set_eq_insert_aux carr x sym by blast
    2.90 +  thus "insert x A {.=} insert x' A"
    2.91 +    using set_eq_def by blast
    2.92 +qed  
    2.93  
    2.94  lemma (in equivalence) set_eq_pairI:
    2.95    assumes xx': "x .= x'"
    2.96      and carr: "x \<in> carrier S" "x' \<in> carrier S" "y \<in> carrier S"
    2.97    shows "{x, y} {.=} {x', y}"
    2.98 -unfolding set_eq_def elem_def
    2.99 -proof safe
   2.100 -  have "x' \<in> {x', y}" by fast
   2.101 -  with xx' show "\<exists>b\<in>{x', y}. x .= b" by fast
   2.102 -next
   2.103 -  have "y \<in> {x', y}" by fast
   2.104 -  with carr show "\<exists>b\<in>{x', y}. y .= b" by fast
   2.105 -next
   2.106 -  have "x \<in> {x, y}" by fast
   2.107 -  with xx'[symmetric] carr
   2.108 -  show "\<exists>a\<in>{x, y}. x' .= a" by fast
   2.109 -next
   2.110 -  have "y \<in> {x, y}" by fast
   2.111 -  with carr show "\<exists>a\<in>{x, y}. y .= a" by fast
   2.112 -qed
   2.113 +  using assms set_eq_insert by simp
   2.114  
   2.115  lemma (in equivalence) is_closedI:
   2.116 -  assumes closed: "!!x y. [| x .= y; x \<in> A; y \<in> carrier S |] ==> y \<in> A"
   2.117 +  assumes closed: "\<And>x y. \<lbrakk>x .= y; x \<in> A; y \<in> carrier S\<rbrakk> \<Longrightarrow> y \<in> A"
   2.118      and S: "A \<subseteq> carrier S"
   2.119    shows "is_closed A"
   2.120    unfolding eq_is_closed_def eq_closure_of_def elem_def
   2.121 @@ -312,19 +307,19 @@
   2.122    by (blast dest: closed sym)
   2.123  
   2.124  lemma (in equivalence) closure_of_eq:
   2.125 -  "[| x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> closure_of A"
   2.126 +  "\<lbrakk>x .= x'; A \<subseteq> carrier S; x \<in> closure_of A; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> closure_of A"
   2.127    unfolding eq_closure_of_def elem_def
   2.128    by (blast intro: trans sym)
   2.129  
   2.130  lemma (in equivalence) is_closed_eq [dest]:
   2.131 -  "[| x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x' \<in> A"
   2.132 +  "\<lbrakk>x .= x'; x \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x' \<in> A"
   2.133    unfolding eq_is_closed_def
   2.134    using closure_of_eq [where A = A]
   2.135    by simp
   2.136  
   2.137  lemma (in equivalence) is_closed_eq_rev [dest]:
   2.138 -  "[| x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S |] ==> x \<in> A"
   2.139 -  by (drule sym) (simp_all add: is_closed_eq)
   2.140 +  "\<lbrakk>x .= x'; x' \<in> A; is_closed A; x \<in> carrier S; x' \<in> carrier S\<rbrakk> \<Longrightarrow> x \<in> A"
   2.141 +  by (meson subsetD eq_is_closed_def is_closed_eq sym)
   2.142  
   2.143  lemma closure_of_closed [simp, intro]:
   2.144    fixes S (structure)
   2.145 @@ -334,81 +329,55 @@
   2.146  
   2.147  lemma closure_of_memI:
   2.148    fixes S (structure)
   2.149 -  assumes "a .\<in> A"
   2.150 -    and "a \<in> carrier S"
   2.151 +  assumes "a .\<in> A" and "a \<in> carrier S"
   2.152    shows "a \<in> closure_of A"
   2.153 -unfolding eq_closure_of_def
   2.154 -using assms
   2.155 -by fast
   2.156 +  by (simp add: assms eq_closure_of_def)
   2.157  
   2.158  lemma closure_ofI2:
   2.159    fixes S (structure)
   2.160 -  assumes "a .= a'"
   2.161 -    and "a' \<in> A"
   2.162 -    and "a \<in> carrier S"
   2.163 +  assumes "a .= a'" and "a' \<in> A" and "a \<in> carrier S"
   2.164    shows "a \<in> closure_of A"
   2.165 -unfolding eq_closure_of_def elem_def
   2.166 -using assms
   2.167 -by fast
   2.168 +  by (meson assms closure_of_memI elem_def)
   2.169  
   2.170  lemma closure_of_memE:
   2.171    fixes S (structure)
   2.172 -  assumes p: "a \<in> closure_of A"
   2.173 -    and r: "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
   2.174 +  assumes "a \<in> closure_of A"
   2.175 +    and "\<lbrakk>a \<in> carrier S; a .\<in> A\<rbrakk> \<Longrightarrow> P"
   2.176    shows "P"
   2.177 -proof -
   2.178 -  from p
   2.179 -      have acarr: "a \<in> carrier S"
   2.180 -      and "a .\<in> A"
   2.181 -      by (simp add: eq_closure_of_def)+
   2.182 -  thus "P" by (rule r)
   2.183 -qed
   2.184 +  using eq_closure_of_def assms by fastforce
   2.185  
   2.186  lemma closure_ofE2:
   2.187    fixes S (structure)
   2.188 -  assumes p: "a \<in> closure_of A"
   2.189 -    and r: "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
   2.190 +  assumes "a \<in> closure_of A"
   2.191 +    and "\<And>a'. \<lbrakk>a \<in> carrier S; a' \<in> A; a .= a'\<rbrakk> \<Longrightarrow> P"
   2.192    shows "P"
   2.193 -proof -
   2.194 -  from p have acarr: "a \<in> carrier S" by (simp add: eq_closure_of_def)
   2.195 +  by (meson closure_of_memE elemE assms)
   2.196  
   2.197 -  from p have "\<exists>a'\<in>A. a .= a'" by (simp add: eq_closure_of_def elem_def)
   2.198 -  from this obtain a'
   2.199 -      where "a' \<in> A" and "a .= a'" by auto
   2.200 -
   2.201 -  from acarr and this
   2.202 -      show "P" by (rule r)
   2.203 +lemma (in equivalence) closure_inclusion:
   2.204 +  assumes "A \<subseteq> B"
   2.205 +  shows "closure_of A \<subseteq> closure_of B"
   2.206 +  unfolding eq_closure_of_def
   2.207 +proof
   2.208 +  fix x
   2.209 +  assume "x \<in> {y \<in> carrier S. y .\<in> A}"
   2.210 +  hence "x \<in> carrier S \<and> x .\<in> A"
   2.211 +    by blast
   2.212 +  hence "x \<in> carrier S \<and> x .\<in> B"
   2.213 +    using assms elem_subsetD by blast
   2.214 +  thus "x \<in> {y \<in> carrier S. y .\<in> B}"
   2.215 +    by simp
   2.216  qed
   2.217  
   2.218 -(*
   2.219 -lemma (in equivalence) classes_consistent:
   2.220 -  assumes Acarr: "A \<subseteq> carrier S"
   2.221 -  shows "is_closed (closure_of A)"
   2.222 -apply (blast intro: elemI elim elemE)
   2.223 -using assms
   2.224 -apply (intro is_closedI closure_of_memI, simp)
   2.225 - apply (elim elemE closure_of_memE)
   2.226 -proof -
   2.227 -  fix x a' a''
   2.228 -  assume carr: "x \<in> carrier S" "a' \<in> carrier S"
   2.229 -  assume a''A: "a'' \<in> A"
   2.230 -  with Acarr have "a'' \<in> carrier S" by fast
   2.231 -  note [simp] = carr this Acarr
   2.232 -
   2.233 -  assume "x .= a'"
   2.234 -  also assume "a' .= a''"
   2.235 -  also from a''A
   2.236 -       have "a'' .\<in> A" by (simp add: elem_exact)
   2.237 -  finally show "x .\<in> A" by simp
   2.238 -qed
   2.239 -*)
   2.240 -(*
   2.241  lemma (in equivalence) classes_small:
   2.242    assumes "is_closed B"
   2.243      and "A \<subseteq> B"
   2.244    shows "closure_of A \<subseteq> B"
   2.245 -using assms
   2.246 -by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE)
   2.247 +proof-
   2.248 +  have "closure_of A \<subseteq> closure_of B"
   2.249 +    using closure_inclusion assms by simp
   2.250 +  thus "closure_of A \<subseteq> B"
   2.251 +    using assms(1) eq_is_closed_def by fastforce
   2.252 +qed
   2.253  
   2.254  lemma (in equivalence) classes_eq:
   2.255    assumes "A \<subseteq> carrier S"
   2.256 @@ -419,9 +388,21 @@
   2.257  lemma (in equivalence) complete_classes:
   2.258    assumes c: "is_closed A"
   2.259    shows "A = closure_of A"
   2.260 -using assms
   2.261 -by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE)
   2.262 -*)
   2.263 +  using assms by (simp add: eq_is_closed_def)
   2.264 +
   2.265 +lemma (in equivalence) closure_idemp_weak:
   2.266 +  "closure_of (closure_of A) {.=} closure_of A"
   2.267 +  by (simp add: classes_eq set_eq_sym)
   2.268 +
   2.269 +lemma (in equivalence) closure_idemp_strong:
   2.270 +  assumes "A \<subseteq> carrier S"
   2.271 +  shows "closure_of (closure_of A) = closure_of A"
   2.272 +  using assms closure_of_eq complete_classes is_closedI by auto
   2.273 +
   2.274 +lemma (in equivalence) complete_classes2:
   2.275 +  assumes "A \<subseteq> carrier S"
   2.276 +  shows "is_closed (closure_of A)"
   2.277 +  using closure_idemp_strong by (simp add: assms eq_is_closed_def)
   2.278  
   2.279  lemma equivalence_subset:
   2.280    assumes "equivalence L" "A \<subseteq> carrier L"
     3.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Tue Apr 17 22:35:48 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Apr 18 15:57:36 2018 +0100
     3.3 @@ -1,12 +1,12 @@
     3.4  theory Change_Of_Vars
     3.5 -  imports  "HOL-Analysis.Vitali_Covering_Theorem" "HOL-Analysis.Determinants"
     3.6 +  imports Vitali_Covering_Theorem Determinants
     3.7  
     3.8  begin
     3.9  
    3.10  subsection\<open>Induction on matrix row operations\<close>
    3.11  
    3.12  lemma induct_matrix_row_operations:
    3.13 -  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
    3.14 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
    3.15    assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
    3.16      and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
    3.17      and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
    3.18 @@ -115,7 +115,7 @@
    3.19  qed
    3.20  
    3.21  lemma induct_matrix_elementary:
    3.22 -  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
    3.23 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
    3.24    assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
    3.25      and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
    3.26      and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
    3.27 @@ -146,7 +146,7 @@
    3.28  qed
    3.29  
    3.30  lemma induct_matrix_elementary_alt:
    3.31 -  fixes P :: "(real^'n, 'n::finite) vec \<Rightarrow> bool"
    3.32 +  fixes P :: "real^'n^'n \<Rightarrow> bool"
    3.33    assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
    3.34      and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
    3.35      and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
    3.36 @@ -196,14 +196,14 @@
    3.37      then show "P (( *v) (A ** B))"
    3.38        by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear)
    3.39    next
    3.40 -    fix A :: "((real, 'n) vec, 'n) vec" and i
    3.41 +    fix A :: "real^'n^'n" and i
    3.42      assume "row i A = 0"
    3.43      then show "P (( *v) A)"
    3.44        by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes)
    3.45    next
    3.46 -    fix A :: "((real, 'n) vec, 'n) vec"
    3.47 +    fix A :: "real^'n^'n"
    3.48      assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
    3.49 -    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x :: "(real, 'n) vec" and i :: "'n"
    3.50 +    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
    3.51        by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
    3.52      then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
    3.53        by (auto simp: 0 matrix_vector_mult_def)
    3.54 @@ -214,7 +214,7 @@
    3.55      assume "m \<noteq> n"
    3.56      have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
    3.57                (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
    3.58 -      for i and x :: "(real, 'n) vec"
    3.59 +      for i and x :: "real^'n"
    3.60        unfolding swap_def by (rule sum.cong) auto
    3.61      have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
    3.62        by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
    3.63 @@ -223,7 +223,7 @@
    3.64    next
    3.65      fix m n :: "'n"
    3.66      assume "m \<noteq> n"
    3.67 -    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "(real, 'n) vec"
    3.68 +    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
    3.69        by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
    3.70      then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
    3.71                 (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
    3.72 @@ -390,7 +390,7 @@
    3.73              using True by auto
    3.74            have "ball 0 B \<subseteq> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
    3.75            proof clarsimp
    3.76 -            fix x :: "(real, 'n) vec"
    3.77 +            fix x :: "real^'n"
    3.78              assume x: "norm x < B"
    3.79              have [simp]: "\<bar>Max (range (\<lambda>k. \<bar>m k\<bar>))\<bar> = Max (range (\<lambda>k. \<bar>m k\<bar>))"
    3.80                by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI)
    3.81 @@ -452,8 +452,6 @@
    3.82  
    3.83  
    3.84  
    3.85 -
    3.86 -
    3.87  proposition
    3.88   fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
    3.89    assumes "linear f" "S \<in> lmeasurable"
    3.90 @@ -473,7 +471,7 @@
    3.91        using f [OF gS] g [OF S] matrix_compose [OF \<open>linear g\<close> \<open>linear f\<close>]
    3.92        by (simp add: o_def image_comp abs_mult det_mul)
    3.93    next
    3.94 -    fix f :: "(real, 'n) vec \<Rightarrow> (real, 'n) vec" and i and S :: "(real, 'n) vec set"
    3.95 +    fix f :: "real^'n::_ \<Rightarrow> real^'n::_" and i and S :: "(real^'n::_) set"
    3.96      assume "linear f" and 0: "\<And>x. f x $ i = 0" and "S \<in> lmeasurable"
    3.97      then have "\<not> inj f"
    3.98        by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component)
    3.99 @@ -490,7 +488,7 @@
   3.100        finally show "?Q f S" .
   3.101      qed
   3.102    next
   3.103 -    fix c and S :: "(real, 'n) vec set"
   3.104 +    fix c and S :: "(real^'n::_) set"
   3.105      assume "S \<in> lmeasurable"
   3.106      show "(\<lambda>a. \<chi> i. c i * a $ i) ` S \<in> lmeasurable \<and> ?Q (\<lambda>a. \<chi> i. c i * a $ i) S"
   3.107      proof
   3.108 @@ -532,7 +530,7 @@
   3.109          using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force+
   3.110      qed
   3.111    next
   3.112 -    fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
   3.113 +    fix m n :: "'n" and S :: "(real, 'n) vec set"
   3.114      assume "m \<noteq> n" and "S \<in> lmeasurable"
   3.115      let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. if i = m then v $ m + v $ n else v $ i"
   3.116      have lin: "linear ?h"
   3.117 @@ -616,26 +614,6 @@
   3.118      by (simp add: measure_linear_image \<open>linear f\<close> S f)
   3.119  qed
   3.120  
   3.121 -lemma sets_lebesgue_inner_closed:
   3.122 -  assumes "S \<in> sets lebesgue" "e > 0"
   3.123 -  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
   3.124 -proof -
   3.125 -  have "-S \<in> sets lebesgue"
   3.126 -    using assms by (simp add: Compl_in_sets_lebesgue)
   3.127 -  then obtain T where "open T" "-S \<subseteq> T"
   3.128 -          and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
   3.129 -    using lmeasurable_outer_open assms  by blast
   3.130 -  show thesis
   3.131 -  proof
   3.132 -    show "closed (-T)"
   3.133 -      using \<open>open T\<close> by blast
   3.134 -    show "-T \<subseteq> S"
   3.135 -      using \<open>- S \<subseteq> T\<close> by auto
   3.136 -    show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
   3.137 -      using T by (auto simp: Int_commute)
   3.138 -  qed
   3.139 -qed
   3.140 -
   3.141  subsection\<open>@{text F_sigma} and @{text G_delta} sets.\<close>
   3.142  
   3.143  (*https://en.wikipedia.org/wiki/F\<sigma>_set*)
   3.144 @@ -645,7 +623,6 @@
   3.145  inductive gdelta :: "'a::topological_space set \<Rightarrow> bool" where
   3.146    "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
   3.147  
   3.148 -
   3.149  lemma fsigma_Union_compact:
   3.150    fixes S :: "'a::{real_normed_vector,heine_borel} set"
   3.151    shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
   3.152 @@ -698,12 +675,9 @@
   3.153      by (simp add: 1 gdelta.intros open_closed)
   3.154  qed
   3.155  
   3.156 -
   3.157 -
   3.158  lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
   3.159    using fsigma_imp_gdelta gdelta_imp_fsigma by force
   3.160  
   3.161 -
   3.162  text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
   3.163  lemma lebesgue_set_almost_fsigma:
   3.164    assumes "S \<in> sets lebesgue"
   3.165 @@ -1839,7 +1813,7 @@
   3.166            using \<open>r > 0\<close> \<open>d > 0\<close> by auto
   3.167          show "{x' \<in> S. \<exists>v. v \<noteq> 0 \<and> (\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {x'}. norm (x' - z) < e \<longrightarrow> \<bar>v \<bullet> (z - x')\<bar> < \<xi> * norm (x' - z))} \<inter> ball x (min d r) \<subseteq> ?W"
   3.168            proof (clarsimp simp: dist_norm norm_minus_commute)
   3.169 -            fix y :: "(real, 'm) vec" and w :: "(real, 'm) vec"
   3.170 +            fix y w 
   3.171              assume "y \<in> S" "w \<noteq> 0"
   3.172                and less [rule_format]:
   3.173                      "\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {y}. norm (y - z) < e \<longrightarrow> \<bar>w \<bullet> (z - y)\<bar> < \<xi> * norm (y - z)"
     4.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Apr 17 22:35:48 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Apr 18 15:57:36 2018 +0100
     4.3 @@ -1297,6 +1297,26 @@
     4.4    qed
     4.5  qed
     4.6  
     4.7 +lemma sets_lebesgue_inner_closed:
     4.8 +  assumes "S \<in> sets lebesgue" "e > 0"
     4.9 +  obtains T where "closed T" "T \<subseteq> S" "S-T \<in> lmeasurable" "measure lebesgue (S - T) < e"
    4.10 +proof -
    4.11 +  have "-S \<in> sets lebesgue"
    4.12 +    using assms by (simp add: Compl_in_sets_lebesgue)
    4.13 +  then obtain T where "open T" "-S \<subseteq> T"
    4.14 +          and T: "(T - -S) \<in> lmeasurable" "measure lebesgue (T - -S) < e"
    4.15 +    using lmeasurable_outer_open assms  by blast
    4.16 +  show thesis
    4.17 +  proof
    4.18 +    show "closed (-T)"
    4.19 +      using \<open>open T\<close> by blast
    4.20 +    show "-T \<subseteq> S"
    4.21 +      using \<open>- S \<subseteq> T\<close> by auto
    4.22 +    show "S - ( -T) \<in> lmeasurable" "measure lebesgue (S - (- T)) < e"
    4.23 +      using T by (auto simp: Int_commute)
    4.24 +  qed
    4.25 +qed
    4.26 +
    4.27  lemma lebesgue_openin:
    4.28     "\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
    4.29    by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel)