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
```