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"