# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1434232127 -3600
# Node ID ba9b52abdddb540989a766361efb5474d848b5e0
# Parent  310853646597beaad3d552edc6d65377c9c3daf1
fixed another horrible proof

diff -r 310853646597 -r ba9b52abdddb src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Jun 13 22:48:47 2015 +0100
@@ -3829,7 +3829,7 @@
 
 lemma iterate_eq_neutral:
   assumes "monoidal opp"
-      and "\<forall>x \<in> s. f x = neutral opp"
+      and "\<And>x. x \<in> s \<Longrightarrow> f x = neutral opp"
     shows "iterate opp s f = neutral opp"
 proof -
   have [simp]: "support opp f s = {}"
@@ -3880,231 +3880,174 @@
 lemma operative_division:
   fixes f :: "'a::euclidean_space set \<Rightarrow> 'b"
   assumes "monoidal opp"
-    and "operative opp f"
-    and "d division_of (cbox a b)"
-  shows "iterate opp d f = f (cbox a b)"
+      and "operative opp f"
+      and "d division_of (cbox a b)"
+    shows "iterate opp d f = f (cbox a b)"
 proof -
   def C \<equiv> "card (division_points (cbox a b) d)"
   then show ?thesis
     using assms
-  proof (induct C arbitrary: a b d rule: full_nat_induct)
-    case goal1
-    { presume *: "content (cbox a b) \<noteq> 0 \<Longrightarrow> ?case"
-      then show ?case
-        apply -
-        apply cases
-        defer
-        apply assumption
-      proof -
-        assume as: "content (cbox a b) = 0"
-        show ?case
-          unfolding operativeD(1)[OF assms(2) as]
-          apply(rule iterate_eq_neutral[OF goal1(2)])
-        proof
-          fix x
-          assume x: "x \<in> d"
-          then guess u v
-            apply (drule_tac division_ofD(4)[OF goal1(4)])
-            apply (elim exE)
-            done
-          then show "f x = neutral opp"
-            using division_of_content_0[OF as goal1(4)]
-            using operativeD(1)[OF assms(2)] x
-            by auto
-        qed
-      qed
-    }
-    assume "content (cbox a b) \<noteq> 0" note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
-    then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-      by (auto intro!: less_imp_le)
+  proof (induct C arbitrary: a b d rule: full_nat_induct) 
+    case (1 a b d)
     show ?case
-    proof (cases "division_points (cbox a b) d = {}")
+    proof (cases "content (cbox a b) = 0")
       case True
-      have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
-        (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
-        unfolding forall_in_division[OF goal1(4)]
-        apply rule
-        apply rule
-        apply rule
-        apply (rule_tac x=a in exI)
-        apply (rule_tac x=b in exI)
-        apply rule
-        apply (rule refl)
-      proof
-        fix u v
-        fix j :: 'a
-        assume j: "j \<in> Basis"
-        assume as: "cbox u v \<in> d"
-        note division_ofD(3)[OF goal1(4) this]
-        then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
-          using j unfolding box_ne_empty by auto
-        have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
-          using as j by auto
-        have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
-          "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
-        note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
-        note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
-        moreover
-        have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
-          using division_ofD(2,2,3)[OF goal1(4) as]
-          unfolding subset_eq
-          apply -
-          apply (erule_tac x=u in ballE,erule_tac[3] x=v in ballE)
-          unfolding box_ne_empty mem_box
-          using j
+      show "iterate opp d f = f (cbox a b)"
+        unfolding operativeD(1)[OF assms(2) True]
+      proof (rule iterate_eq_neutral[OF `monoidal opp`]) 
+        fix x
+        assume x: "x \<in> d"
+        then show "f x = neutral opp" 
+          by (metis division_ofD(4) 1(4) division_of_content_0[OF True] operativeD(1)[OF assms(2)] x)
+      qed
+    next
+      case False
+      note ab = this[unfolded content_lt_nz[symmetric] content_pos_lt_eq]
+      then have ab': "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
+        by (auto intro!: less_imp_le)
+        show "iterate opp d f = f (cbox a b)"
+      proof (cases "division_points (cbox a b) d = {}")
+        case True
+        { fix u v and j :: 'a
+          assume j: "j \<in> Basis" and as: "cbox u v \<in> d"
+          then have "cbox u v \<noteq> {}"
+            using "1.prems"(3) by blast
+          then have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "u\<bullet>j \<le> v\<bullet>j"
+            using j unfolding box_ne_empty by auto
+          have *: "\<And>p r Q. \<not> j\<in>Basis \<or> p \<or> r \<or> (\<forall>x\<in>d. Q x) \<Longrightarrow> p \<or> r \<or> Q (cbox u v)"
+            using as j by auto
+          have "(j, u\<bullet>j) \<notin> division_points (cbox a b) d"
+               "(j, v\<bullet>j) \<notin> division_points (cbox a b) d" using True by auto
+          note this[unfolded de_Morgan_conj division_points_def mem_Collect_eq split_conv interval_bounds[OF ab'] bex_simps]
+          note *[OF this(1)] *[OF this(2)] note this[unfolded interval_bounds[OF uv(1)]]
+          moreover
+          have "a\<bullet>j \<le> u\<bullet>j" "v\<bullet>j \<le> b\<bullet>j"
+            using division_ofD(2,2,3)[OF `d division_of cbox a b` as]
+            apply (metis j subset_box(1) uv(1))
+            by (metis `cbox u v \<subseteq> cbox a b` j subset_box(1) uv(1))
+          ultimately have "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
+            unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force }
+        then have d': "\<forall>i\<in>d. \<exists>u v. i = cbox u v \<and>
+          (\<forall>j\<in>Basis. u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j)"
+          unfolding forall_in_division[OF 1(4)]
+          by blast 
+        have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
+          unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
+        note this[unfolded division_ofD(6)[OF `d division_of cbox a b`,symmetric] Union_iff]
+        then guess i .. note i=this
+        guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
+        have "cbox a b \<in> d"
+        proof -
+          have "u = a" "v = b"
+            unfolding euclidean_eq_iff[where 'a='a]
+          proof safe
+            fix j :: 'a
+            assume j: "j \<in> Basis"
+            note i(2)[unfolded uv mem_box,rule_format,of j]
+            then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
+              using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
+          qed
+          then have "i = cbox a b" using uv by auto
+          then show ?thesis using i by auto
+        qed
+        then have deq: "d = insert (cbox a b) (d - {cbox a b})"
+          by auto
+        have "iterate opp (d - {cbox a b}) f = neutral opp"
+        proof (rule iterate_eq_neutral[OF 1(2)])
+          fix x
+          assume x: "x \<in> d - {cbox a b}"
+          then have "x\<in>d"
+            by auto note d'[rule_format,OF this]
+          then guess u v by (elim exE conjE) note uv=this
+          have "u \<noteq> a \<or> v \<noteq> b"
+            using x[unfolded uv] by auto
+          then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
+            unfolding euclidean_eq_iff[where 'a='a] by auto
+          then have "u\<bullet>j = v\<bullet>j"
+            using uv(2)[rule_format,OF j] by auto
+          then have "content (cbox u v) = 0"
+            unfolding content_eq_0 using j
+            by force
+          then show "f x = neutral opp"
+            unfolding uv(1) by (rule operativeD(1)[OF 1(3)])
+        qed
+        then show "iterate opp d f = f (cbox a b)"
+          apply (subst deq)
+          apply (subst iterate_insert[OF 1(2)])
+          using 1
           apply auto
           done
-        ultimately show "u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = a\<bullet>j \<or> u\<bullet>j = b\<bullet>j \<and> v\<bullet>j = b\<bullet>j \<or> u\<bullet>j = a\<bullet>j \<and> v\<bullet>j = b\<bullet>j"
-          unfolding not_less de_Morgan_disj using ab[rule_format,of j] uv(2) j by force
-      qed
-      have "(1/2) *\<^sub>R (a+b) \<in> cbox a b"
-        unfolding mem_box using ab by(auto intro!: less_imp_le simp: inner_simps)
-      note this[unfolded division_ofD(6)[OF goal1(4),symmetric] Union_iff]
-      then guess i .. note i=this
-      guess u v using d'[rule_format,OF i(1)] by (elim exE conjE) note uv=this
-      have "cbox a b \<in> d"
-      proof -
-        { presume "i = cbox a b" then show ?thesis using i by auto }
-        { presume "u = a" "v = b" then show "i = cbox a b" using uv by auto }
-        show "u = a" "v = b"
-          unfolding euclidean_eq_iff[where 'a='a]
-        proof safe
-          fix j :: 'a
-          assume j: "j \<in> Basis"
-          note i(2)[unfolded uv mem_box,rule_format,of j]
-          then show "u \<bullet> j = a \<bullet> j" and "v \<bullet> j = b \<bullet> j"
-            using uv(2)[rule_format,of j] j by (auto simp: inner_simps)
-        qed
-      qed
-      then have *: "d = insert (cbox a b) (d - {cbox a b})"
-        by auto
-      have "iterate opp (d - {cbox a b}) f = neutral opp"
-        apply (rule iterate_eq_neutral[OF goal1(2)])
-      proof
-        fix x
-        assume x: "x \<in> d - {cbox a b}"
-        then have "x\<in>d"
-          by auto note d'[rule_format,OF this]
-        then guess u v by (elim exE conjE) note uv=this
-        have "u \<noteq> a \<or> v \<noteq> b"
-          using x[unfolded uv] by auto
-        then obtain j where "u\<bullet>j \<noteq> a\<bullet>j \<or> v\<bullet>j \<noteq> b\<bullet>j" and j: "j \<in> Basis"
-          unfolding euclidean_eq_iff[where 'a='a] by auto
-        then have "u\<bullet>j = v\<bullet>j"
-          using uv(2)[rule_format,OF j] by auto
-        then have "content (cbox u v) = 0"
-          unfolding content_eq_0
-          apply (rule_tac x=j in bexI)
-          using j
-          apply auto
+      next
+        case False
+        then have "\<exists>x. x \<in> division_points (cbox a b) d"
+          by auto
+        then guess k c
+          unfolding split_paired_Ex division_points_def mem_Collect_eq split_conv
+          apply (elim exE conjE)
+          done
+        note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
+        from this(3) guess j .. note j=this
+        def d1 \<equiv> "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
+        def d2 \<equiv> "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
+        def cb \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)::'a"
+        def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
+        note division_points_psubset[OF `d division_of cbox a b` ab kc(1-2) j]
+        note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
+        then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
+          "(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+          unfolding interval_split[OF kc(4)]
+          apply (rule_tac[!] "1.hyps"[rule_format])
+          using division_split[OF `d division_of cbox a b`, where k=k and c=c]
+          apply (simp_all add: interval_split 1 kc d1_def d2_def division_points_finite[OF `d division_of cbox a b`])
           done
-        then show "f x = neutral opp"
-          unfolding uv(1) by (rule operativeD(1)[OF goal1(3)])
+        { fix l y
+          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
+          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+          have "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
+            unfolding leq interval_split[OF kc(4)]
+            apply (rule operativeD(1) 1)+
+            unfolding interval_split[symmetric,OF kc(4)]
+            using division_split_left_inj 1 as kc leq by blast 
+        } note fxk_le = this
+        { fix l y
+          assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
+          from division_ofD(4)[OF `d division_of cbox a b` this(1)] guess u v by (elim exE) note leq=this
+          have "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
+            unfolding leq interval_split[OF kc(4)]
+            apply (rule operativeD(1) 1)+
+            unfolding interval_split[symmetric,OF kc(4)]
+            using division_split_right_inj 1 leq as kc by blast
+        } note fxk_ge = this
+        have "f (cbox a b) = opp (iterate opp d1 f) (iterate opp d2 f)" (is "_ = ?prev")
+          unfolding *
+          using assms(2) kc(4) by blast
+        also have "iterate opp d1 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<le> c}))"
+          unfolding d1_def empty_as_interval
+          apply (rule iterate_nonzero_image_lemma[unfolded o_def])
+          apply (rule 1 division_of_finite operativeD[OF 1(3)])+
+          apply (force simp add: empty_as_interval[symmetric] fxk_le)+
+          done
+        also have "iterate opp d2 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<ge> c}))"
+          unfolding d2_def empty_as_interval
+          apply (rule iterate_nonzero_image_lemma[unfolded o_def])
+          apply (rule 1 division_of_finite operativeD[OF 1(3)])+
+          apply (force simp add: empty_as_interval[symmetric] fxk_ge)+
+          done
+        also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
+          unfolding forall_in_division[OF `d division_of cbox a b`]
+          using assms(2) kc(4) by blast
+        have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
+          iterate opp d f"
+          apply (subst(3) iterate_eq[OF _ *[rule_format]])
+          using 1
+          apply (auto simp: iterate_op[symmetric])
+          done
+        finally show ?thesis by auto
       qed
-      then show "iterate opp d f = f (cbox a b)"
-        apply -
-        apply (subst *)
-        apply (subst iterate_insert[OF goal1(2)])
-        using goal1(2,4)
-        apply auto
-        done
-    next
-      case False
-      then have "\<exists>x. x \<in> division_points (cbox a b) d"
-        by auto
-      then guess k c
-        unfolding split_paired_Ex
-        unfolding division_points_def mem_Collect_eq split_conv
-        apply (elim exE conjE)
-        done
-      note this(2-4,1) note kc=this[unfolded interval_bounds[OF ab']]
-      from this(3) guess j .. note j=this
-      def d1 \<equiv> "{l \<inter> {x. x\<bullet>k \<le> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<le> c} \<noteq> {}}"
-      def d2 \<equiv> "{l \<inter> {x. x\<bullet>k \<ge> c} | l. l \<in> d \<and> l \<inter> {x. x\<bullet>k \<ge> c} \<noteq> {}}"
-      def cb \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else b\<bullet>i) *\<^sub>R i)::'a"
-      def ca \<equiv> "(\<Sum>i\<in>Basis. (if i = k then c else a\<bullet>i) *\<^sub>R i)::'a"
-      note division_points_psubset[OF goal1(4) ab kc(1-2) j]
-      note psubset_card_mono[OF _ this(1)] psubset_card_mono[OF _ this(2)]
-      then have *: "(iterate opp d1 f) = f (cbox a b \<inter> {x. x\<bullet>k \<le> c})"
-        "(iterate opp d2 f) = f (cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
-        unfolding interval_split[OF kc(4)]
-        apply (rule_tac[!] goal1(1)[rule_format])
-        using division_split[OF goal1(4), where k=k and c=c]
-        unfolding interval_split[OF kc(4)] d1_def[symmetric] d2_def[symmetric]
-        unfolding goal1(2) Suc_le_mono
-        using goal1(2-3)
-        using division_points_finite[OF goal1(4)]
-        using kc(4)
-        apply auto
-        done
-      have "f (cbox a b) = opp (iterate opp d1 f) (iterate opp d2 f)" (is "_ = ?prev")
-        unfolding *
-        apply (rule operativeD(2))
-        using goal1(3)
-        using kc(4)
-        apply auto
-        done
-      also have "iterate opp d1 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<le> c}))"
-        unfolding d1_def
-        apply (rule iterate_nonzero_image_lemma[unfolded o_def])
-        unfolding empty_as_interval
-        apply (rule goal1 division_of_finite operativeD[OF goal1(3)])+
-        unfolding empty_as_interval[symmetric]
-        apply (rule content_empty)
-      proof (rule, rule, rule, erule conjE)
-        fix l y
-        assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. x \<bullet> k \<le> c} = y \<inter> {x. x \<bullet> k \<le> c}" "l \<noteq> y"
-        from division_ofD(4)[OF goal1(4) this(1)] guess u v by (elim exE) note l=this
-        show "f (l \<inter> {x. x \<bullet> k \<le> c}) = neutral opp"
-          unfolding l interval_split[OF kc(4)]
-          apply (rule operativeD(1) goal1)+
-          unfolding interval_split[symmetric,OF kc(4)]
-          apply (rule division_split_left_inj)
-          apply (rule goal1)
-          unfolding l[symmetric]
-          apply (rule as(1), rule as(2))
-          apply (rule kc(4) as)+
-          done
-      qed
-      also have "iterate opp d2 f = iterate opp d (\<lambda>l. f(l \<inter> {x. x\<bullet>k \<ge> c}))"
-        unfolding d2_def
-        apply (rule iterate_nonzero_image_lemma[unfolded o_def])
-        unfolding empty_as_interval
-        apply (rule goal1 division_of_finite operativeD[OF goal1(3)])+
-        unfolding empty_as_interval[symmetric]
-        apply (rule content_empty)
-      proof (rule, rule, rule, erule conjE)
-        fix l y
-        assume as: "l \<in> d" "y \<in> d" "l \<inter> {x. c \<le> x \<bullet> k} = y \<inter> {x. c \<le> x \<bullet> k}" "l \<noteq> y"
-        from division_ofD(4)[OF goal1(4) this(1)] guess u v by (elim exE) note l=this
-        show "f (l \<inter> {x. x \<bullet> k \<ge> c}) = neutral opp"
-        unfolding l interval_split[OF kc(4)]
-          apply (rule operativeD(1) goal1)+
-          unfolding interval_split[symmetric,OF kc(4)]
-          apply (rule division_split_right_inj)
-          apply (rule goal1)
-          unfolding l[symmetric]
-          apply (rule as(1))
-          apply (rule as(2))
-          apply (rule as kc(4))+
-          done
-      qed also have *: "\<forall>x\<in>d. f x = opp (f (x \<inter> {x. x \<bullet> k \<le> c})) (f (x \<inter> {x. c \<le> x \<bullet> k}))"
-        unfolding forall_in_division[OF goal1(4)]
-        apply (rule, rule, rule, rule operativeD(2))
-        using goal1(3) kc
-        by auto
-      have "opp (iterate opp d (\<lambda>l. f (l \<inter> {x. x \<bullet> k \<le> c}))) (iterate opp d (\<lambda>l. f (l \<inter> {x. c \<le> x \<bullet> k}))) =
-        iterate opp d f"
-        apply (subst(3) iterate_eq[OF _ *[rule_format]])
-        prefer 3
-        apply (rule iterate_op[symmetric])
-        using goal1
-        apply auto
-        done
-      finally show ?thesis by auto
-    qed
-  qed
-qed
+    qed
+  qed
+qed
+
 
 lemma iterate_image_nonzero:
   assumes "monoidal opp"
@@ -8350,7 +8293,7 @@
   note * = this[unfolded neutral_add]
   have iterate:"iterate (lifted op +) (p - {cbox c d})
     (\<lambda>i. if g integrable_on i then Some (integral i g) else None) = Some 0"
-  proof (rule *, rule)
+  proof (rule *)
     case goal1
     then have "x \<in> p"
       by auto