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