src/HOL/Multivariate_Analysis/Integration.thy
changeset 39302 d7728f65b353
parent 38656 d5d342611edb
child 40163 a462d5207aa6
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -102,7 +102,7 @@
     1.4  abbreviation One  where "One \<equiv> ((\<chi>\<chi> i. 1)::_::ordered_euclidean_space)"
     1.5  
     1.6  lemma empty_as_interval: "{} = {One..0}"
     1.7 -  apply(rule set_ext,rule) defer unfolding mem_interval
     1.8 +  apply(rule set_eqI,rule) defer unfolding mem_interval
     1.9    using UNIV_witness[where 'a='n] apply(erule_tac exE,rule_tac x=x in allE) by auto
    1.10  
    1.11  lemma interior_subset_union_intervals: 
    1.12 @@ -367,7 +367,7 @@
    1.13  let ?A = "{s. s \<in>  (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" have *:"?A' = ?A" by auto
    1.14  show ?thesis unfolding * proof(rule division_ofI) have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto
    1.15    moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto ultimately show "finite ?A" by auto
    1.16 -  have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_ext) unfolding * and Union_image_eq UN_iff
    1.17 +  have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_eqI) unfolding * and Union_image_eq UN_iff
    1.18      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
    1.19    { fix k assume "k\<in>?A" then obtain k1 k2 where k:"k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto thus "k \<noteq> {}" by auto
    1.20    show "k \<subseteq> s1 \<inter> s2" using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] unfolding k by auto
    1.21 @@ -1035,7 +1035,7 @@
    1.22        next assume as:"c $$ i = (a $$ i + b $$ i) / 2" "d $$ i = b $$ i"
    1.23          show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
    1.24        qed qed qed
    1.25 -  also have "\<Union> ?A = {a..b}" proof(rule set_ext,rule)
    1.26 +  also have "\<Union> ?A = {a..b}" proof(rule set_eqI,rule)
    1.27      fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff ..
    1.28      from this(1) guess c unfolding mem_Collect_eq .. then guess d ..
    1.29      note c_d = this[THEN conjunct2,rule_format] `x\<in>Y`[unfolded this[THEN conjunct1]]
    1.30 @@ -1402,7 +1402,7 @@
    1.31    apply(rule integral_unique) using has_integral_empty .
    1.32  
    1.33  lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a::'a::ordered_euclidean_space}"
    1.34 -proof- have *:"{a} = {a..a}" apply(rule set_ext) unfolding mem_interval singleton_iff euclidean_eq[where 'a='a]
    1.35 +proof- have *:"{a} = {a..a}" apply(rule set_eqI) unfolding mem_interval singleton_iff euclidean_eq[where 'a='a]
    1.36      apply safe prefer 3 apply(erule_tac x=i in allE) by(auto simp add: field_simps)
    1.37    show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
    1.38      apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
    1.39 @@ -1466,7 +1466,7 @@
    1.40  lemma interval_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
    1.41    "{a..b} \<inter> {x. x$$k \<le> c} = {a .. (\<chi>\<chi> i. if i = k then min (b$$k) c else b$$i)}"
    1.42    "{a..b} \<inter> {x. x$$k \<ge> c} = {(\<chi>\<chi> i. if i = k then max (a$$k) c else a$$i) .. b}"
    1.43 -  apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval mem_Collect_eq using assms by auto
    1.44 +  apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval mem_Collect_eq using assms by auto
    1.45  
    1.46  lemma content_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
    1.47    "content {a..b} = content({a..b} \<inter> {x. x$$k \<le> c}) + content({a..b} \<inter> {x. x$$k >= c})"
    1.48 @@ -2494,7 +2494,7 @@
    1.49    note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
    1.50    note division_split(2)[OF this, where c="c-e" and k=k,OF k] 
    1.51    thus ?thesis apply(rule **) using k apply- unfolding interval_doublesplit unfolding * unfolding interval_split interval_doublesplit
    1.52 -    apply(rule set_ext) unfolding mem_Collect_eq apply rule apply(erule conjE exE)+ apply(rule_tac x=la in exI) defer
    1.53 +    apply(rule set_eqI) unfolding mem_Collect_eq apply rule apply(erule conjE exE)+ apply(rule_tac x=la in exI) defer
    1.54      apply(erule conjE exE)+ apply(rule_tac x="l \<inter> {x. c + e \<ge> x $$ k}" in exI) apply rule defer apply rule
    1.55      apply(rule_tac x=l in exI) by blast+ qed
    1.56  
    1.57 @@ -2538,7 +2538,7 @@
    1.58        apply(cases,rule disjI1,assumption,rule disjI2)
    1.59      proof- fix x l assume as:"(x,l)\<in>p" "?i x \<noteq> 0" hence xk:"x$$k = c" unfolding indicator_def apply-by(rule ccontr,auto)
    1.60        show "content l = content (l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d})" apply(rule arg_cong[where f=content])
    1.61 -        apply(rule set_ext,rule,rule) unfolding mem_Collect_eq
    1.62 +        apply(rule set_eqI,rule,rule) unfolding mem_Collect_eq
    1.63        proof- fix y assume y:"y\<in>l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
    1.64          note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this]
    1.65          thus "\<bar>y $$ k - c\<bar> \<le> d" unfolding euclidean_simps xk by auto
    1.66 @@ -3280,7 +3280,7 @@
    1.67  proof(cases "{a..b}={}") case True thus ?thesis unfolding True by auto
    1.68  next have *:"\<And>P Q. (\<forall>i<DIM('a). P i) \<and> (\<forall>i<DIM('a). Q i) \<longleftrightarrow> (\<forall>i<DIM('a). P i \<and> Q i)" by auto
    1.69    case False note ab = this[unfolded interval_ne_empty]
    1.70 -  show ?thesis apply-apply(rule set_ext)
    1.71 +  show ?thesis apply-apply(rule set_eqI)
    1.72    proof- fix x::"'a" have **:"\<And>P Q. (\<forall>i<DIM('a). P i = Q i) \<Longrightarrow> (\<forall>i<DIM('a). P i) = (\<forall>i<DIM('a). Q i)" by auto
    1.73      show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" unfolding if_not_P[OF False] 
    1.74        unfolding image_iff mem_interval Bex_def euclidean_simps euclidean_eq[where 'a='a] *
    1.75 @@ -3334,7 +3334,7 @@
    1.76  subsection {* even more special cases. *}
    1.77  
    1.78  lemma uminus_interval_vector[simp]:"uminus ` {a..b} = {-b .. -a::'a::ordered_euclidean_space}"
    1.79 -  apply(rule set_ext,rule) defer unfolding image_iff
    1.80 +  apply(rule set_eqI,rule) defer unfolding image_iff
    1.81    apply(rule_tac x="-x" in bexI) by(auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a])
    1.82  
    1.83  lemma has_integral_reflect_lemma[intro]: assumes "(f has_integral i) {a..b}"
    1.84 @@ -3694,7 +3694,7 @@
    1.85    let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
    1.86    { presume *:"a<b \<Longrightarrow> ?thesis"
    1.87      show ?thesis apply(cases,rule *,assumption)
    1.88 -    proof- case goal1 hence "{a..b} = {x}" using as(1) apply-apply(rule set_ext)
    1.89 +    proof- case goal1 hence "{a..b} = {x}" using as(1) apply-apply(rule set_eqI)
    1.90          unfolding atLeastAtMost_iff by(auto simp only:field_simps not_less DIM_real)
    1.91        thus ?case using `e>0` by auto
    1.92      qed } assume "a<b"