src/HOL/Multivariate_Analysis/Integration.thy
changeset 50252 4aa34bd43228
parent 50241 8b0fdeeefef7
child 50348 4b4fe0d5ee22
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Nov 28 15:38:12 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Nov 28 15:59:18 2012 +0100
     1.3 @@ -867,11 +867,11 @@
     1.4    guess \<pi> using ex_bij_betw_nat_finite_1[OF finite_lessThan[of "DIM('a)"]] .. note \<pi>=this
     1.5    def \<pi>' \<equiv> "inv_into {1..n} \<pi>"
     1.6    have \<pi>':"bij_betw \<pi>' {..<DIM('a)} {1..n}" using bij_betw_inv_into[OF \<pi>] unfolding \<pi>'_def n_def by auto
     1.7 -  hence \<pi>'i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
     1.8 -  have \<pi>i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
     1.9 -  have \<pi>\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def
    1.10 +  hence \<pi>'_i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
    1.11 +  have \<pi>_i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
    1.12 +  have \<pi>_\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def
    1.13      apply(rule f_inv_into_f) unfolding n_def using \<pi> unfolding bij_betw_def by auto
    1.14 -  have \<pi>'\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq)
    1.15 +  have \<pi>'_\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq)
    1.16      using \<pi> unfolding n_def bij_betw_def by auto
    1.17    have "{c..d} \<noteq> {}" using assms by auto
    1.18    let ?p1 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else if \<pi>' i = l then c$$\<pi> l else b$$i)}"
    1.19 @@ -943,47 +943,47 @@
    1.20        assume "l \<le> l'" fix x
    1.21        have "x \<notin> interior k \<inter> interior k'" 
    1.22        proof(rule,cases "l' = n+1") assume x:"x \<in> interior k \<inter> interior k'"
    1.23 -        case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'i using l' by(auto simp add:less_Suc_eq_le)
    1.24 +        case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'_i using l' by(auto simp add:less_Suc_eq_le)
    1.25          hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l' then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
    1.26          hence k':"k' = {c..d}" using l'(1) unfolding * by auto
    1.27          have ln:"l < n + 1" 
    1.28          proof(rule ccontr) case goal1 hence l2:"l = n+1" using l by auto
    1.29 -          hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'i by(auto simp add:less_Suc_eq_le)
    1.30 +          hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'_i by(auto simp add:less_Suc_eq_le)
    1.31            hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
    1.32 -          hence "k = {c..d}" using l(1) \<pi>'i unfolding * by(auto)
    1.33 +          hence "k = {c..d}" using l(1) \<pi>'_i unfolding * by(auto)
    1.34            thus False using `k\<noteq>k'` k' by auto
    1.35 -        qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'\<pi>[of l] using l ln by auto
    1.36 +        qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'_\<pi>[of l] using l ln by auto
    1.37          have "x $$ \<pi> l < c $$ \<pi> l \<or> d $$ \<pi> l < x $$ \<pi> l" using l(1) apply-
    1.38          proof(erule disjE)
    1.39            assume as:"k = ?p1 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.40 -          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] by(auto simp add:** not_less)
    1.41 +          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>_i[of l] by(auto simp add:** not_less)
    1.42          next assume as:"k = ?p2 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.43 -          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] unfolding ** by auto
    1.44 +          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>_i[of l] unfolding ** by auto
    1.45          qed thus False using x unfolding k' unfolding Int_iff interior_closed_interval mem_interval
    1.46            by(auto elim!:allE[where x="\<pi> l"])
    1.47        next case False hence "l < n + 1" using l'(2) using `l\<le>l'` by auto
    1.48          hence ln:"l \<in> {1..n}" "l' \<in> {1..n}" using l l' False by auto
    1.49 -        note \<pi>l = \<pi>'\<pi>[OF ln(1)] \<pi>'\<pi>[OF ln(2)]
    1.50 +        note \<pi>_l = \<pi>'_\<pi>[OF ln(1)] \<pi>'_\<pi>[OF ln(2)]
    1.51          assume x:"x \<in> interior k \<inter> interior k'"
    1.52          show False using l(1) l'(1) apply-
    1.53          proof(erule_tac[!] disjE)+
    1.54            assume as:"k = ?p1 l" "k' = ?p1 l'"
    1.55            note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.56            have "l \<noteq> l'" using k'(2)[unfolded as] by auto
    1.57 -          thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>i[OF ln(1)] \<pi>i[OF ln(2)] apply(cases "l<l'")
    1.58 -            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
    1.59 +          thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>_i[OF ln(1)] \<pi>_i[OF ln(2)] apply(cases "l<l'")
    1.60 +            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
    1.61          next assume as:"k = ?p2 l" "k' = ?p2 l'"
    1.62            note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.63            have "l \<noteq> l'" apply(rule) using k'(2)[unfolded as] by auto
    1.64 -          thus False using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
    1.65 +          thus False using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
    1.66          next assume as:"k = ?p1 l" "k' = ?p2 l'"
    1.67            note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.68            show False using abcd[of "\<pi> l'"] using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln apply(cases "l=l'")
    1.69 -            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
    1.70 +            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
    1.71          next assume as:"k = ?p2 l" "k' = ?p1 l'"
    1.72            note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
    1.73            show False using *[of "\<pi> l"] *[of "\<pi> l'"] ln `l \<le> l'` apply(cases "l=l'") using abcd[of "\<pi> l'"] 
    1.74 -            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
    1.75 +            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
    1.76          qed qed } 
    1.77      from this[OF k l k' l'] this[OF k'(1) l' k _ l] have "\<And>x. x \<notin> interior k \<inter> interior k'"
    1.78        apply - apply(cases "l' \<le> l") using k'(2) by auto