src/HOL/Multivariate_Analysis/Integration.thy
 changeset 36362 06475a1547cb parent 36359 e5c785c166b2 child 36365 18bf20d0c2df
```     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Apr 25 23:22:29 2010 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Apr 26 09:21:25 2010 -0700
1.3 @@ -933,7 +933,7 @@
1.4  lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
1.5    shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
1.6  proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
1.7 -    unfolding vec_sub Cart_eq by(auto simp add:vec1_dest_vec1_simps split_beta)
1.8 +    unfolding vec_sub Cart_eq by(auto simp add: split_beta)
1.9    show ?thesis using assms unfolding has_integral apply safe
1.10      apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
1.11      apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
1.12 @@ -1356,7 +1356,7 @@
1.13
1.14  lemma has_integral_eq_eq:
1.15    shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
1.16 -  using has_integral_eq[of s f g] has_integral_eq[of s g f] by auto
1.17 +  using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
1.18
1.19  lemma has_integral_null[dest]:
1.20    assumes "content({a..b}) = 0" shows  "(f has_integral 0) ({a..b})"
1.21 @@ -1653,7 +1653,7 @@
1.22  proof- have *:"{a..b} = ({a..b} \<inter> {x. x\$k \<le> c}) \<union> ({a..b} \<inter> {x. x\$k \<ge> c})" by auto
1.23    show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms])
1.24      unfolding interval_split interior_closed_interval
1.25 -    by(auto simp add: vector_less_def Cart_lambda_beta elim!:allE[where x=k]) qed
1.26 +    by(auto simp add: vector_less_def elim!:allE[where x=k]) qed
1.27
1.28  lemma has_integral_separate_sides: fixes f::"real^'m \<Rightarrow> 'a::real_normed_vector"
1.29    assumes "(f has_integral i) ({a..b})" "e>0"
1.30 @@ -1743,11 +1743,11 @@
1.31  subsection {* Using additivity of lifted function to encode definedness. *}
1.32
1.33  lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
1.34 -  by (metis map_of.simps option.nchotomy)
1.35 +  by (metis option.nchotomy)
1.36
1.37  lemma exists_option:
1.38   "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
1.39 -  by (metis map_of.simps option.nchotomy)
1.40 +  by (metis option.nchotomy)
1.41
1.42  fun lifted where
1.43    "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
1.44 @@ -1842,9 +1842,8 @@
1.45  lemma operative_content[intro]: "operative (op +) content"
1.46    unfolding operative_def content_split[THEN sym] neutral_add by auto
1.47
1.48 -lemma neutral_monoid[simp]: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
1.49 -  unfolding neutral_def apply(rule some_equality) defer
1.50 -  apply(erule_tac x=0 in allE) by auto
1.51 +lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
1.52 +  by (rule neutral_add) (* FIXME: duplicate *)
1.53
1.54  lemma monoidal_monoid[intro]:
1.55    shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
1.56 @@ -1941,7 +1940,7 @@
1.57      apply(rule_tac x="(k,(interval_lowerbound l)\$k)" in exI) defer
1.58      apply(rule_tac x="(k,(interval_upperbound l)\$k)" in exI)
1.59      unfolding division_points_def unfolding interval_bounds[OF ab]
1.60 -    apply (auto simp add:interval_bounds) unfolding * by auto
1.61 +    apply auto unfolding * by auto
1.62    thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto
1.63
1.64    have *:"interval_lowerbound ({a..b} \<inter> {x. x \$ k \<ge> interval_lowerbound l \$ k}) \$ k = interval_lowerbound l \$ k"
1.65 @@ -1952,7 +1951,7 @@
1.66      apply(rule_tac x="(k,(interval_lowerbound l)\$k)" in exI) defer
1.67      apply(rule_tac x="(k,(interval_upperbound l)\$k)" in exI)
1.68      unfolding division_points_def unfolding interval_bounds[OF ab]
1.69 -    apply (auto simp add:interval_bounds) unfolding * by auto
1.70 +    apply auto unfolding * by auto
1.71    thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto qed
1.72
1.73  subsection {* Preservation by divisions and tagged divisions. *}
1.74 @@ -2254,7 +2253,7 @@
1.75    assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)\$i \<le> (g x)\$i"
1.76    shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)\$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)\$i"
1.77    unfolding setsum_component apply(rule setsum_mono)
1.78 -  apply(rule mp) defer apply assumption apply(induct_tac x,rule) unfolding split_conv
1.79 +  apply(rule mp) defer apply assumption unfolding split_paired_all apply rule unfolding split_conv
1.80  proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
1.81    from this(3) guess u v apply-by(erule exE)+ note b=this
1.82    show "(content b *\<^sub>R f a) \$ i \<le> (content b *\<^sub>R g a) \$ i" unfolding b
1.83 @@ -2903,7 +2902,7 @@
1.84    shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
1.85  proof- let ?f = "(\<lambda>k::(real^1) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
1.86    have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty_1
1.87 -    by(auto simp add:not_less interval_bound_1 vector_less_def)
1.88 +    by(auto simp add:not_less vector_less_def)
1.89    have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
1.90    note * = this[unfolded if_not_P[OF **] interval_bound_1[OF assms(1)],THEN sym ]
1.91    show ?thesis unfolding * apply(subst setsum_iterate[THEN sym]) defer
1.92 @@ -3340,7 +3339,7 @@
1.93  proof- { presume *:"a < b \<Longrightarrow> ?thesis"
1.94      show ?thesis proof(cases,rule *,assumption)
1.95        assume "\<not> a < b" hence "a = b" using assms(1) by auto
1.96 -      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" apply(auto simp add: Cart_simps) by smt
1.97 +      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" by(auto simp add: Cart_eq vector_le_def order_antisym)
1.98        show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0_1 using * `a=b` by auto
1.99      qed } assume ab:"a < b"
1.100    let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {vec1 a..vec1 b} \<and> d fine p \<longrightarrow>
1.101 @@ -3422,7 +3421,7 @@
1.102          hence "\<forall>i. u\$i \<le> v\$i" and uv:"{u,v}\<subseteq>{u..v}" using p(2)[OF as(1)] by auto note this(1) this(1)[unfolded forall_1]
1.103          note result = as(2)[unfolded k interval_bounds[OF this(1)] content_1[OF this(2)]]
1.104
1.105 -        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x\$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add:Cart_simps) note  * = d(2)[OF this]
1.106 +        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x\$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add: Cart_eq) note  * = d(2)[OF this]
1.107          have "norm ((v\$1 - u\$1) *\<^sub>R f' (x\$1) - (f (v\$1) - f (u\$1))) =
1.108            norm ((f (u\$1) - f (x\$1) - (u\$1 - x\$1) *\<^sub>R f' (x\$1)) - (f (v\$1) - f (x\$1) - (v\$1 - x\$1) *\<^sub>R f' (x\$1)))"
1.109            apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto
1.110 @@ -3669,7 +3668,7 @@
1.111      from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
1.112      show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
1.113        unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
1.114 -  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
1.115 +  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: vector_less_def)
1.116      from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
1.117      from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
1.118      show ?thesis apply(rule_tac x="min d1 d2" in exI)
1.119 @@ -3726,7 +3725,7 @@
1.120      unfolding o_def using assms(5) defer apply-apply(rule)
1.121    proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
1.122      have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps])
1.123 -      using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
1.124 +      using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
1.125      have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
1.126        apply(rule diff_chain_within) apply(rule has_derivative_add)
1.127        unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
1.128 @@ -3949,7 +3948,7 @@
1.129
1.130  lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
1.131    assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
1.132 -  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
1.133 +  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
1.134
1.135  lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
1.136    assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
```