src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63945 444eafb6e864
parent 63944 21eaff8c8fc9
child 63956 b235e845c8e8
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 26 16:57:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Sep 27 16:24:53 2016 +0100
     1.3 @@ -503,7 +503,7 @@
     1.4        obtain a2 b2 where k2: "k2 = cbox a2 b2"
     1.5          using division_ofD(4)[OF assms(2) k(3)] by blast
     1.6        show "\<exists>a b. k = cbox a b"
     1.7 -        unfolding k k1 k2 unfolding inter_interval by auto
     1.8 +        unfolding k k1 k2 unfolding Int_interval by auto
     1.9      }
    1.10      fix k1 k2
    1.11      assume "k1 \<in> ?A"
    1.12 @@ -826,7 +826,7 @@
    1.13    next
    1.14      case False
    1.15      obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
    1.16 -      unfolding inter_interval by auto
    1.17 +      unfolding Int_interval by auto
    1.18      have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
    1.19      obtain p where "p division_of cbox c d" "cbox u v \<in> p"
    1.20        by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
    1.21 @@ -4733,34 +4733,21 @@
    1.22  
    1.23  subsection \<open>Some other trivialities about negligible sets.\<close>
    1.24  
    1.25 -lemma negligible_subset[intro]:
    1.26 -  assumes "negligible s"
    1.27 -    and "t \<subseteq> s"
    1.28 +lemma negligible_subset:
    1.29 +  assumes "negligible s" "t \<subseteq> s"
    1.30    shows "negligible t"
    1.31    unfolding negligible_def
    1.32 -proof (safe, goal_cases)
    1.33 -  case (1 a b)
    1.34 -  show ?case
    1.35 -    using assms(1)[unfolded negligible_def,rule_format,of a b]
    1.36 -    apply -
    1.37 -    apply (rule has_integral_spike[OF assms(1)])
    1.38 -    defer
    1.39 -    apply assumption
    1.40 -    using assms(2)
    1.41 -    unfolding indicator_def
    1.42 -    apply auto
    1.43 -    done
    1.44 -qed
    1.45 +    by (metis (no_types) Diff_iff assms contra_subsetD has_integral_negligible indicator_simps(2))
    1.46  
    1.47  lemma negligible_diff[intro?]:
    1.48    assumes "negligible s"
    1.49    shows "negligible (s - t)"
    1.50 -  using assms by auto
    1.51 +  using assms by (meson Diff_subset negligible_subset)
    1.52  
    1.53  lemma negligible_Int:
    1.54    assumes "negligible s \<or> negligible t"
    1.55    shows "negligible (s \<inter> t)"
    1.56 -  using assms by auto
    1.57 +  using assms negligible_subset by force
    1.58  
    1.59  lemma negligible_Un:
    1.60    assumes "negligible s"
    1.61 @@ -4780,10 +4767,10 @@
    1.62  qed
    1.63  
    1.64  lemma negligible_Un_eq[simp]: "negligible (s \<union> t) \<longleftrightarrow> negligible s \<and> negligible t"
    1.65 -  using negligible_Un by auto
    1.66 +  using negligible_Un negligible_subset by blast 
    1.67  
    1.68  lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}"
    1.69 -  using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] by auto
    1.70 +  using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
    1.71  
    1.72  lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> negligible s"
    1.73    apply (subst insert_is_Un)
    1.74 @@ -4792,7 +4779,7 @@
    1.75    done
    1.76  
    1.77  lemma negligible_empty[iff]: "negligible {}"
    1.78 -  by auto
    1.79 +  using negligible_insert by blast
    1.80  
    1.81  lemma negligible_finite[intro]:
    1.82    assumes "finite s"
    1.83 @@ -7652,7 +7639,7 @@
    1.84        apply auto
    1.85        done
    1.86    qed
    1.87 -qed auto
    1.88 +qed (simp add: negligible_Int)
    1.89  
    1.90  lemma negligible_translation:
    1.91    assumes "negligible S"
    1.92 @@ -7689,32 +7676,24 @@
    1.93    apply (rule has_integral_spike_eq[OF assms])
    1.94    by (auto split: if_split_asm)
    1.95  
    1.96 -lemma has_integral_spike_set[dest]:
    1.97 +lemma has_integral_spike_set:
    1.98    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.99 -  assumes "negligible ((s - t) \<union> (t - s))"
   1.100 -    and "(f has_integral y) s"
   1.101 +  assumes "(f has_integral y) s" "negligible ((s - t) \<union> (t - s))"
   1.102    shows "(f has_integral y) t"
   1.103    using assms has_integral_spike_set_eq
   1.104    by auto
   1.105  
   1.106 -lemma integrable_spike_set[dest]:
   1.107 +lemma integrable_spike_set:
   1.108    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.109 -  assumes "negligible ((s - t) \<union> (t - s))"
   1.110 -    and "f integrable_on s"
   1.111 -  shows "f integrable_on t"
   1.112 -  using assms(2)
   1.113 -  unfolding integrable_on_def
   1.114 -  unfolding has_integral_spike_set_eq[OF assms(1)] .
   1.115 +  assumes "f integrable_on s" and "negligible ((s - t) \<union> (t - s))"
   1.116 +    shows "f integrable_on t"
   1.117 +  using assms by (simp add: integrable_on_def has_integral_spike_set_eq)
   1.118  
   1.119  lemma integrable_spike_set_eq:
   1.120    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.121    assumes "negligible ((s - t) \<union> (t - s))"
   1.122    shows "f integrable_on s \<longleftrightarrow> f integrable_on t"
   1.123 -  apply rule
   1.124 -  apply (rule_tac[!] integrable_spike_set)
   1.125 -  using assms
   1.126 -  apply auto
   1.127 -  done
   1.128 +by (blast intro: integrable_spike_set assms negligible_subset)
   1.129  
   1.130  (*lemma integral_spike_set:
   1.131   "\<forall>f:real^M->real^N g s t.