author paulson Mon, 26 Jun 2017 16:59:44 +0100 changeset 66193 6e6eeef63589 parent 66192 e5b84854baa4 child 66197 c8604c9f3a8a
More tidying of horrible proofs
```--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 26 14:26:03 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 26 16:59:44 2017 +0100
@@ -2224,8 +2224,8 @@
have "\<exists>x. \<forall>n. x \<in> convex hull {fa n, fb n, fc n}"
apply (rule bounded_closed_nest)
apply (simp_all add: compact_imp_closed finite_imp_compact_convex_hull finite_imp_bounded_convex_hull)
-      apply (rule allI)
-      apply (rule transitive_stepwise_le)
+      apply (intro allI impI)
+      apply (erule transitive_stepwise_le)
apply (auto simp: conv_le)
done
then obtain x where x: "\<And>n. x \<in> convex hull {fa n, fb n, fc n}" by auto```
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 26 14:26:03 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Jun 26 16:59:44 2017 +0100
@@ -1673,7 +1673,7 @@
assume "(x, k) \<in> p'"
then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
show "x \<in> k" and "k \<subseteq> cbox a b"
using p'(2-3)[OF il(3)] il by auto
show "\<exists>a b. k = cbox a b"
@@ -1687,12 +1687,12 @@
assume "(x1, k1) \<in> p'"
then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
unfolding p'_def by auto
-        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
+        then obtain i1 l1 where il1: "x1 \<in> i1" "i1 \<in> d" "(x1, l1) \<in> p" "k1 = i1 \<inter> l1" by blast
fix x2 k2
assume "(x2,k2)\<in>p'"
then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
unfolding p'_def by auto
-        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
+        then obtain i2 l2 where il2: "x2 \<in> i2" "i2 \<in> d" "(x2, l2) \<in> p" "k2 = i2 \<inter> l2" by blast
assume "(x1, k1) \<noteq> (x2, k2)"
then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
@@ -1768,7 +1768,7 @@
assume "(x, k) \<in> p'"
then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        then obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "k = i \<inter> l" by blast
then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
apply (rule_tac x=x in exI)
apply (rule_tac x=i in exI)```
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jun 26 14:26:03 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Jun 26 16:59:44 2017 +0100
@@ -9,6 +9,10 @@
Lebesgue_Measure Tagged_Division
begin

+(*FIXME DELETE*)
+lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
+lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
+
(* try instead structured proofs below *)
lemma norm_diff2: "\<lbrakk>y = y1 + y2; x = x1 + x2; e = e1 + e2; norm(y1 - x1) \<le> e1; norm(y2 - x2) \<le> e2\<rbrakk>
\<Longrightarrow> norm(y - x) \<le> e"
@@ -1611,7 +1615,8 @@
have "bounded (ball 0 B1 \<union> ball (0::'a) B2)"
unfolding bounded_Un by(rule conjI bounded_ball)+
from bounded_subset_cbox[OF this] guess a b by (elim exE)
-      note ab = conjunctD2[OF this[unfolded Un_subset_iff]]
+      then have ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
+        by blast+
guess w1 using B(2)[OF ab(1)] .. note w1=conjunctD2[OF this]
guess w2 using B(4)[OF ab(2)] .. note w2=conjunctD2[OF this]
have *: "\<And>w1 w2 j i::real .\<bar>w1 - i\<bar> < (i - j) / 3 \<Longrightarrow> \<bar>w2 - j\<bar> < (i - j) / 3 \<Longrightarrow> w1 \<le> w2 \<Longrightarrow> False"
@@ -6267,7 +6272,7 @@
apply (rule *)
unfolding eventually_sequentially
apply (rule_tac x=k in exI)
-      apply -
+      apply clarify
apply (rule transitive_stepwise_le)
using assms(2)[rule_format, OF x]
apply auto
@@ -6290,7 +6295,8 @@
apply (rule trivial_limit_sequentially)
unfolding eventually_sequentially
apply (rule_tac x=k in exI)
-    apply (rule transitive_stepwise_le)
+    apply clarify
+    apply (erule transitive_stepwise_le)
prefer 3
unfolding inner_simps real_inner_1_right
apply (rule integral_le)
@@ -6490,11 +6496,7 @@
then have "y \<in> cbox a b"
using p'(3)[OF xk] by auto
then have *: "\<And>m. \<forall>n\<ge>m. f m y \<le> f n y"
-            apply -
-            apply (rule transitive_stepwise_le)
-            using assms(2)
-            apply auto
-            done
+            using assms(2) by (auto intro: transitive_stepwise_le)
show "f r y \<le> f (m x) y" and "f (m x) y \<le> f s y"
apply (rule_tac[!] *[rule_format])
using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk]
@@ -6536,10 +6538,7 @@
apply (rule trivial_limit_sequentially)
unfolding eventually_sequentially
apply (rule_tac x=k in exI)
-      apply (rule transitive_stepwise_le)
-      using that(3)
-      apply auto
-      done
+      using assms(3) by (force intro: transitive_stepwise_le)
note fg=this[rule_format]

have "\<exists>i. ((\<lambda>k. integral s (f k)) \<longlongrightarrow> i) sequentially"
@@ -6553,11 +6552,7 @@
done
then guess i .. note i=this
have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x"
-      apply rule
-      apply (rule transitive_stepwise_le)
-      using that(3)
-      apply auto
-      done
+      using assms(3) by (force intro: transitive_stepwise_le)
then have i': "\<forall>k. (integral s (f k))\<bullet>1 \<le> i\<bullet>1"
apply -
apply rule
@@ -6682,10 +6677,7 @@
proof (safe, goal_cases)
case (2 x)
have "\<And>m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. (f m x)\<bullet>1 \<le> (f n x)\<bullet>1"
-            apply (rule transitive_stepwise_le)
-            using assms(3)
-            apply auto
-            done
+            using assms(3) by (force intro: transitive_stepwise_le)
then show ?case
by auto
next
@@ -6715,10 +6707,7 @@
apply rule
done
have "\<And>x m. x \<in> s \<Longrightarrow> \<forall>n\<ge>m. f m x \<le> f n x"
-    apply (rule transitive_stepwise_le)
-    using assms(2)
-    apply auto
-    done
+    using assms(2) by (force intro: transitive_stepwise_le)
note * = this[rule_format]
have "(\<lambda>x. g x - f 0 x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) \<longlongrightarrow>
integral s (\<lambda>x. g x - f 0 x)) sequentially"```
```--- a/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 26 14:26:03 2017 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Mon Jun 26 16:59:44 2017 +0100
@@ -87,23 +87,13 @@
qed

-lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
-lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
-lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
-
-lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
-  by auto
-
declare norm_triangle_ineq4[intro]

lemma transitive_stepwise_le:
-  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
-  shows "\<forall>n\<ge>m. R m n"
-proof (intro allI impI)
-  show "m \<le> n \<Longrightarrow> R m n" for n
-    by (induction rule: dec_induct)
-       (use assms in blast)+
-qed
+  assumes "m \<le> n" "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
+  shows "R m n"
+using \<open>m \<le> n\<close>
+  by (induction rule: dec_induct) (use assms in blast)+

subsection \<open>Some useful lemmas about intervals.\<close>

@@ -367,14 +357,13 @@
unfolding division_of_def cbox_sing by auto
next
assume ?l
-  note * = conjunctD4[OF this[unfolded division_of_def cbox_sing]]
{
fix x
assume x: "x \<in> s" have "x = {a}"
-      using *(2)[rule_format,OF x] by auto
+      by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD x)
}
moreover have "s \<noteq> {}"
-    using *(4) by auto
+    using \<open>s division_of cbox a a\<close> by auto
ultimately show ?r
unfolding cbox_sing by auto
qed
@@ -2235,7 +2224,7 @@
apply blast
done
define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
-  have "A 0 = a" "B 0 = b" "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
+  have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
(\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i)" (is "\<And>n. ?P n")
proof -
@@ -2261,8 +2250,12 @@
done
qed
qed
-  note AB = this(1-2) conjunctD2[OF this(3),rule_format]
-
+  then have AB: "A(n)\<bullet>i \<le> A(Suc n)\<bullet>i" "A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i"
+                 "B(Suc n)\<bullet>i \<le> B(n)\<bullet>i" "2 * (B(Suc n)\<bullet>i - A(Suc n)\<bullet>i) \<le> B(n)\<bullet>i - A(n)\<bullet>i"
+                if "i\<in>Basis" for i n
+    using that by blast+
+  have notPAB: "\<not> P (cbox (A(Suc n)) (B(Suc n)))" for n
+    using ABRAW by blast
have interv: "\<exists>n. \<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e"
if e: "0 < e" for e
proof -
@@ -2293,6 +2286,7 @@
next
case (Suc n)
have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
+            using AB(3) that
using AB(4)[of i n] using i by auto
also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
using Suc by (auto simp add: field_simps)
@@ -2310,31 +2304,38 @@
proof (induction rule: inc_induct)
case (step i)
show ?case
-        using AB(4) by (intro order_trans[OF step.IH] subset_box_imp) auto
+        using AB by (intro order_trans[OF step.IH] subset_box_imp) auto
qed simp
} note ABsubset = this
have "\<exists>a. \<forall>n. a\<in> cbox (A n) (B n)"
-    by (rule decreasing_closed_nest[rule_format,OF closed_cbox _ ABsubset interv])
-      (metis nat.exhaust AB(1-3) assms(1,3))
+  proof (rule decreasing_closed_nest)
+    show "\<forall>n. closed (cbox (A n) (B n))"
+    show "\<forall>n. cbox (A n) (B n) \<noteq> {}"
+      by (meson AB dual_order.trans interval_not_empty)
+  qed (use ABsubset interv in auto)
then obtain x0 where x0: "\<And>n. x0 \<in> cbox (A n) (B n)"
by blast
show thesis
proof (rule that[rule_format, of x0])
show "x0\<in>cbox a b"
-      using x0[of 0] unfolding AB .
+      using \<open>A 0 = a\<close> \<open>B 0 = b\<close> x0 by blast
fix e :: real
assume "e > 0"
from interv[OF this] obtain n
where n: "\<forall>x\<in>cbox (A n) (B n). \<forall>y\<in>cbox (A n) (B n). dist x y < e" ..
have "\<not> P (cbox (A n) (B n))"
-      apply (cases "0 < n")
-      using AB(3)[of "n - 1"] assms(3) AB(1-2)
-      apply auto
-      done
+    proof (cases "0 < n")
+      case True then show ?thesis
+        by (metis Suc_pred' notPAB)
+    next
+      case False then show ?thesis
+        using \<open>A 0 = a\<close> \<open>B 0 = b\<close> \<open>\<not> P (cbox a b)\<close> by blast
+    qed
moreover have "cbox (A n) (B n) \<subseteq> ball x0 e"
using n using x0[of n] by auto
moreover have "cbox (A n) (B n) \<subseteq> cbox a b"
-      unfolding AB(1-2)[symmetric] by (rule ABsubset) auto
+      using ABsubset \<open>A 0 = a\<close> \<open>B 0 = b\<close> by blast
ultimately show "\<exists>c d. x0 \<in> cbox c d \<and> cbox c d \<subseteq> ball x0 e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
apply (rule_tac x="A n" in exI)
apply (rule_tac x="B n" in exI)
@@ -2434,7 +2435,11 @@
case (insert xk p)
guess x k using surj_pair[of xk] by (elim exE) note xk=this
note tagged_partial_division_subset[OF insert(4) subset_insertI]
-    from insert(3)[OF this insert(5)] guess q1 .. note q1 = conjunctD3[OF this]
+    from insert(3)[OF this insert(5)]
+    obtain q1 where q1: "q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}"
+                and "d fine q1"
+                and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p;  k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> q1"
+      by (force simp add: )
have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
unfolding xk by auto
note p = tagged_partial_division_ofD[OF insert(4)]
@@ -2479,19 +2484,7 @@
apply rule
apply (rule fine_Un)
apply (subst fine_def)
-        defer
-        apply (rule q1)
-        unfolding Ball_def split_paired_All split_conv
-        apply rule
-        apply rule
-        apply rule
-        apply rule
-        apply (erule insertE)
-        apply (simp add: uv xk)
-        apply (rule UnI2)
-        apply (drule q1(3)[rule_format])
-        unfolding xk uv
-        apply auto
+         apply (auto simp add:  \<open>d fine q1\<close> q1I uv xk)
done
next
case False
@@ -2501,21 +2494,7 @@
apply rule
unfolding * uv
apply (rule tagged_division_union q2 q1 int fine_Un)+
-        unfolding Ball_def split_paired_All split_conv
-        apply rule
-        apply (rule fine_Un)
-        apply (rule q1 q2)+
-        apply rule
-        apply rule
-        apply rule
-        apply rule
-        apply (erule insertE)
-        apply (rule UnI2)
-        apply (simp add: False uv xk)
-        apply (drule q1(3)[rule_format])
-        using False
-        unfolding xk uv
-        apply auto
+          apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
done
qed
qed```