# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1519058685 0
# Node ID c8caefb20564c67d45a8670c9f1398ca64af2a1e
# Parent  8f4810b9d9d1afffa7a532249f1b0ef34fe7f5dd
lots of new material, ultimately related to measure theory

diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -52,14 +52,6 @@
 lemmas Zero_notin_Suc = zero_notin_Suc_image
 lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
 
-lemma sum_union_disjoint':
-  assumes "finite A"
-    and "finite B"
-    and "A \<inter> B = {}"
-    and "A \<union> B = C"
-  shows "sum g C = sum g A + sum g B"
-  using sum.union_disjoint[OF assms(1-3)] and assms(4) by auto
-
 lemma pointwise_minimal_pointwise_maximal:
   fixes s :: "(nat \<Rightarrow> nat) set"
   assumes "finite s"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -497,7 +497,7 @@
 lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
   by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
 
-lemma matrix_mul_lid:
+lemma matrix_mul_lid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "mat 1 ** A = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
@@ -507,7 +507,7 @@
   done
 
 
-lemma matrix_mul_rid:
+lemma matrix_mul_rid [simp]:
   fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
   shows "A ** mat 1 = A"
   apply (simp add: matrix_matrix_mult_def mat_def)
@@ -529,7 +529,7 @@
   apply simp
   done
 
-lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
+lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
   apply (vector matrix_vector_mult_def mat_def)
   apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong)
   done
@@ -560,18 +560,18 @@
   apply simp
   done
 
-lemma transpose_mat: "transpose (mat n) = mat n"
+lemma transpose_mat [simp]: "transpose (mat n) = mat n"
   by (vector transpose_def mat_def)
 
 lemma transpose_transpose: "transpose(transpose A) = A"
   by (vector transpose_def)
 
-lemma row_transpose:
+lemma row_transpose [simp]:
   fixes A:: "'a::semiring_1^_^_"
   shows "row i (transpose A) = column i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
 
-lemma column_transpose:
+lemma column_transpose [simp]:
   fixes A:: "'a::semiring_1^_^_"
   shows "column i (transpose A) = row i A"
   by (simp add: row_def column_def transpose_def vec_eq_iff)
@@ -582,12 +582,22 @@
 lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
   by (metis transpose_transpose rows_transpose)
 
+lemma matrix_mult_transpose_dot_column:
+  fixes A :: "real^'n^'n"
+  shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
+
+lemma matrix_mult_transpose_dot_row:
+  fixes A :: "real^'n^'n"
+  shows "A ** transpose A = (\<chi> i j. (row i A) \<bullet> (row j A))"
+  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
+
 text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
 
 lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
   by (simp add: matrix_vector_mult_def inner_vec_def)
 
-lemma matrix_mult_vsum:
+lemma matrix_mult_sum:
   "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
   by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
 
@@ -632,6 +642,37 @@
   by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
       field_simps sum_distrib_left sum.distrib)
 
+lemma matrix_vector_mult_add_distrib [algebra_simps]:
+  fixes A :: "real^'n^'m"
+  shows "A *v (x + y) = A *v x + A *v y"
+  using matrix_vector_mul_linear [of A]  by (simp add: linear_add)
+
+lemma matrix_vector_mult_diff_distrib [algebra_simps]:
+  fixes A :: "real^'n^'m"
+  shows "A *v (x - y) = A *v x - A *v y"
+  using matrix_vector_mul_linear [of A]  by (simp add: linear_diff)
+
+lemma matrix_vector_mult_scaleR[algebra_simps]:
+  fixes A :: "real^'n^'m"
+  shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
+  using linear_iff matrix_vector_mul_linear by blast
+
+lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
+  by (simp add: matrix_vector_mult_def vec_eq_iff)
+
+lemma matrix_vector_mult_0 [simp]: "0 *v w = 0"
+  by (simp add: matrix_vector_mult_def vec_eq_iff)
+
+lemma matrix_vector_mult_add_rdistrib [algebra_simps]:
+  fixes A :: "real^'n^'m"
+  shows "(A + B) *v x = (A *v x) + (B *v x)"
+  by (simp add: vec_eq_iff inner_add_left matrix_vector_mul_component)
+
+lemma matrix_vector_mult_diff_rdistrib [algebra_simps]:
+  fixes A :: "real^'n^'m"
+  shows "(A - B) *v x = (A *v x) - (B *v x)"
+  by (simp add: vec_eq_iff inner_diff_left matrix_vector_mul_component)
+
 lemma matrix_works:
   assumes lf: "linear f"
   shows "matrix f *v x = f (x::real ^ 'n)"
@@ -641,7 +682,7 @@
 lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
   by (simp add: ext matrix_works)
 
-lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
+lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
   by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
 
 lemma matrix_compose:
@@ -768,7 +809,7 @@
       let ?x = "\<chi> i. c i"
       have th0:"A *v ?x = 0"
         using c
-        unfolding matrix_mult_vsum vec_eq_iff
+        unfolding matrix_mult_sum vec_eq_iff
         by auto
       from k[rule_format, OF th0] i
       have "c i = 0" by (vector vec_eq_iff)}
@@ -777,7 +818,7 @@
   { assume H: ?rhs
     { fix x assume x: "A *v x = 0"
       let ?c = "\<lambda>i. ((x$i ):: real)"
-      from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x]
+      from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
       have "x = 0" by vector }
   }
   ultimately show ?thesis unfolding matrix_left_invertible_ker by blast
@@ -798,7 +839,7 @@
   let ?U = "UNIV :: 'm set"
   have fU: "finite ?U" by simp
   have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
-    unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
+    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
     apply (subst eq_commute)
     apply rule
     done
@@ -1002,7 +1043,7 @@
     and "cbox a b = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
   by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis)
 
-lemma mem_interval_cart:
+lemma mem_box_cart:
   fixes a :: "real^'n"
   shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
     and "x \<in> cbox a b \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
@@ -1014,7 +1055,7 @@
     and "(cbox a b = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
 proof -
   { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
-    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
+    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_box_cart by auto
     hence "a$i < b$i" by auto
     hence False using as by auto }
   moreover
@@ -1025,11 +1066,11 @@
       hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
         unfolding vector_smult_component and vector_add_component
         by auto }
-    hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
+    hence "box a b \<noteq> {}" using mem_box_cart(1)[of "?x" a b] by auto }
   ultimately show ?th1 by blast
 
   { fix i x assume as:"b$i < a$i" and x:"x\<in>cbox a b"
-    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval_cart by auto
+    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_box_cart by auto
     hence "a$i \<le> b$i" by auto
     hence False using as by auto }
   moreover
@@ -1040,7 +1081,7 @@
       hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
         unfolding vector_smult_component and vector_add_component
         by auto }
-    hence "cbox a b \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto  }
+    hence "cbox a b \<noteq> {}" using mem_box_cart(2)[of "?x" a b] by auto  }
   ultimately show ?th2 by blast
 qed
 
@@ -1057,7 +1098,7 @@
     and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> cbox c d \<subseteq> box a b"
     and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> cbox a b"
     and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
-  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
+  unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart
   by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
 
 lemma interval_sing:
@@ -1410,7 +1451,7 @@
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
   "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
   apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_interval_cart mem_Collect_eq interval_cbox_cart
+  unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart
   unfolding vec_lambda_beta
   by auto
 
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -3016,28 +3016,6 @@
     using compact_closed_sums[OF compact_sing[of a] assms] by auto
 qed
 
-lemma translation_Compl:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
-  apply (auto simp: image_iff)
-  apply (rule_tac x="x - a" in bexI, auto)
-  done
-
-lemma translation_UNIV:
-  fixes a :: "'a::ab_group_add"
-  shows "range (\<lambda>x. a + x) = UNIV"
-  by (fact surj_plus)
-
-lemma translation_diff:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
-  by auto
-
-lemma translation_Int:
-  fixes a :: "'a::ab_group_add"
-  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
-  by auto
-
 lemma closure_translation:
   fixes a :: "'a::real_normed_vector"
   shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -54,7 +54,7 @@
 
 text \<open>Basic determinant properties.\<close>
 
-lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
+lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
 proof -
   let ?di = "\<lambda>A i j. A$i$j"
   let ?U = "(UNIV :: 'n set)"
@@ -193,33 +193,10 @@
     unfolding det_def by (simp add: sign_id)
 qed
 
-lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
-proof -
-  let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
-  let ?U = "UNIV :: 'n set"
-  let ?f = "\<lambda>i j. ?A$i$j"
-  {
-    fix i
-    assume i: "i \<in> ?U"
-    have "?f i i = 1"
-      using i by (vector mat_def)
-  }
-  then have th: "prod (\<lambda>i. ?f i i) ?U = prod (\<lambda>x. 1) ?U"
-    by (auto intro: prod.cong)
-  {
-    fix i j
-    assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
-    have "?f i j = 0" using i j ij
-      by (vector mat_def)
-  }
-  then have "det ?A = prod (\<lambda>i. ?f i i) ?U"
-    using det_diagonal by blast
-  also have "\<dots> = 1"
-    unfolding th prod.neutral_const ..
-  finally show ?thesis .
-qed
+lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
+  by (simp add: det_diagonal mat_def)
 
-lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
+lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
   by (simp add: det_def prod_zero)
 
 lemma det_permute_rows:
@@ -487,6 +464,21 @@
     done
 qed
 
+lemma matrix_id_mat_1: "matrix id = mat 1"
+  by (simp add: mat_def matrix_def axis_def)
+
+lemma matrix_id [simp]: "det (matrix id) = 1"
+  by (simp add: matrix_id_mat_1)
+
+lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
+  by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
+
+lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
+  apply (subst det_diagonal)
+   apply (auto simp: matrix_def mat_def prod_constant)
+  apply (simp add: cart_eq_inner_axis inner_axis_axis)
+  done
+
 text \<open>
   May as well do this, though it's a bit unsatisfactory since it ignores
   exact duplicates by considering the rows/columns as a set.
@@ -788,7 +780,7 @@
   shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"
   by (metis invertible_def matrix_left_right_inverse)
 
-lemma invertible_righ_inverse:
+lemma invertible_right_inverse:
   fixes A :: "real^'n^'n"
   shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"
   by (metis invertible_def matrix_left_right_inverse)
@@ -800,7 +792,7 @@
   {
     assume "invertible A"
     then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"
-      unfolding invertible_righ_inverse by blast
+      unfolding invertible_right_inverse by blast
     then have "det (A ** B) = det (mat 1 :: real ^'n^'n)"
       by simp
     then have "det A \<noteq> 0"
@@ -815,7 +807,7 @@
     from H obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0"
       and iU: "i \<in> ?U"
       and ci: "c i \<noteq> 0"
-      unfolding invertible_righ_inverse
+      unfolding invertible_right_inverse
       unfolding matrix_right_invertible_independent_rows
       by blast
     have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
@@ -903,7 +895,7 @@
   have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
     by (auto simp add: row_transpose intro: sum.cong)
   show ?thesis
-    unfolding matrix_mult_vsum
+    unfolding matrix_mult_sum
     unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
     unfolding *[of "\<lambda>i. x$i"]
     apply (subst det_transpose[symmetric])
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -118,7 +118,7 @@
   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
   have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}"
     apply (rule set_eqI)
-    unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart
+    unfolding image_iff Bex_def mem_box_cart interval_cbox_cart
     apply rule
     defer
     apply (rule_tac x="vec x" in exI)
@@ -133,7 +133,7 @@
       unfolding image_iff ..
     then have "x \<noteq> 0"
       using as[of "w$1" "w$2"]
-      unfolding mem_interval_cart atLeastAtMost_iff
+      unfolding mem_box_cart atLeastAtMost_iff
       by auto
   } note x0 = this
   have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
@@ -187,7 +187,7 @@
       unfolding *[symmetric] y o_def
       by (rule lem1[rule_format])
     then show "x \<in> cbox (-1) 1"
-      unfolding mem_interval_cart interval_cbox_cart infnorm_2
+      unfolding mem_box_cart interval_cbox_cart infnorm_2
       apply -
       apply rule
     proof -
@@ -241,7 +241,7 @@
   qed
   note lem3 = this[rule_format]
   have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
-    using x(1) unfolding mem_interval_cart by auto
+    using x(1) unfolding mem_box_cart by auto
   then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
     unfolding right_minus_eq
     apply -
@@ -274,7 +274,7 @@
       apply auto
       done
     ultimately show False
-      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
       apply (erule_tac x=1 in allE)
       apply auto
       done
@@ -293,7 +293,7 @@
       apply auto
       done
     ultimately show False
-      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
       apply (erule_tac x=1 in allE)
       apply auto
       done
@@ -312,7 +312,7 @@
       apply auto
       done
     ultimately show False
-      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
       apply (erule_tac x=2 in allE)
       apply auto
       done
@@ -331,7 +331,7 @@
       apply auto
       done
     ultimately show False
-      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
+      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
       apply (erule_tac x=2 in allE)
       apply auto
       done
@@ -426,7 +426,7 @@
     apply (rule pathfinish_in_path_image)
     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
     unfolding pathstart_def
-    apply (auto simp add: less_eq_vec_def mem_interval_cart)
+    apply (auto simp add: less_eq_vec_def mem_box_cart)
     done
   then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
   have "z \<in> cbox a b"
@@ -436,8 +436,8 @@
   then have "z = f 0"
     unfolding vec_eq_iff forall_2
     unfolding z(2) pathstart_def
-    using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
-    unfolding mem_interval_cart
+    using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
+    unfolding mem_box_cart
     apply (erule_tac x=1 in allE)
     using as
     apply auto
@@ -458,7 +458,7 @@
     unfolding assms
     using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
     unfolding pathstart_def
-    apply (auto simp add: less_eq_vec_def mem_interval_cart)
+    apply (auto simp add: less_eq_vec_def mem_box_cart)
     done
   then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   have "z \<in> cbox a b"
@@ -468,8 +468,8 @@
   then have "z = g 0"
     unfolding vec_eq_iff forall_2
     unfolding z(2) pathstart_def
-    using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
-    unfolding mem_interval_cart
+    using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
+    unfolding mem_box_cart
     apply (erule_tac x=2 in allE)
     using as
     apply auto
@@ -745,7 +745,7 @@
     using pathstart_in_path_image pathfinish_in_path_image
     using assms(3-4)
     by auto
-  note startfin = this[unfolded mem_interval_cart forall_2]
+  note startfin = this[unfolded mem_box_cart forall_2]
   let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
      linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
      linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
@@ -791,7 +791,7 @@
       apply (rule Un_least)+
       defer 3
       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval_cart forall_2 vector_2
+      unfolding mem_box_cart forall_2 vector_2
       using ab startfin abab assms(3)
       using assms(9-)
       unfolding assms
@@ -803,7 +803,7 @@
       apply (rule Un_least)+
       defer 2
       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval_cart forall_2 vector_2
+      unfolding mem_box_cart forall_2 vector_2
       using ab startfin abab assms(4)
       using assms(9-)
       unfolding assms
@@ -833,7 +833,7 @@
       have "pathfinish f \<in> cbox a b"
         using assms(3) pathfinish_in_path_image[of f] by auto
       then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
-        unfolding mem_interval_cart forall_2 by auto
+        unfolding mem_box_cart forall_2 by auto
       then have "z$1 \<noteq> pathfinish f$1"
         using prems(2)
         using assms ab
@@ -842,7 +842,7 @@
         using assms(3) pathstart_in_path_image[of f]
         by auto
       then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
-        unfolding mem_interval_cart forall_2
+        unfolding mem_box_cart forall_2
         by auto
       then have "z$1 \<noteq> pathstart f$1"
         using prems(2) using assms ab
@@ -857,7 +857,7 @@
       moreover have "pathstart g \<in> cbox a b"
         using assms(4) pathstart_in_path_image[of g]
         by auto
-      note this[unfolded mem_interval_cart forall_2]
+      note this[unfolded mem_box_cart forall_2]
       then have "z$1 \<noteq> pathstart g$1"
         using prems(1)
         using assms ab
@@ -880,7 +880,7 @@
       by auto
     with z' show "z \<in> path_image f"
       using z(1)
-      unfolding Un_iff mem_interval_cart forall_2
+      unfolding Un_iff mem_box_cart forall_2
       apply -
       apply (simp only: segment_vertical segment_horizontal vector_2)
       unfolding assms
@@ -892,7 +892,7 @@
       by auto
     with z' show "z \<in> path_image g"
       using z(2)
-      unfolding Un_iff mem_interval_cart forall_2
+      unfolding Un_iff mem_box_cart forall_2
       apply (simp only: segment_vertical segment_horizontal vector_2)
       unfolding assms
       apply auto
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -18,6 +18,8 @@
 typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
+declare vec_lambda_inject [simplified, simp]
+
 notation
   vec_nth (infixl "$" 90) and
   vec_lambda (binder "\<chi>" 10)
@@ -54,7 +56,7 @@
 lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f"
   by (auto simp add: vec_eq_iff)
 
-lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g"
+lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
   by (simp add: vec_eq_iff)
 
 subsection \<open>Cardinality of vectors\<close>
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1134,4 +1134,12 @@
   qed
 qed
 
+lemma lebesgue_openin:
+   "\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
+  by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel)
+
+lemma lebesgue_closedin:
+   "\<lbrakk>closedin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
+  by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel)
+
 end
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1749,6 +1749,10 @@
 lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
   using fmeasurableI2[of A M "A - B"] by auto
 
+lemma fmeasurable_Int_fmeasurable:
+   "\<lbrakk>S \<in> fmeasurable M; T \<in> sets M\<rbrakk> \<Longrightarrow> (S \<inter> T) \<in> fmeasurable M"
+  by (meson fmeasurableD fmeasurableI2 inf_le1 sets.Int)
+
 lemma fmeasurable_UN:
   assumes "countable I" "\<And>i. i \<in> I \<Longrightarrow> F i \<subseteq> A" "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M" "A \<in> fmeasurable M"
   shows "(\<Union>i\<in>I. F i) \<in> fmeasurable M"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1099,6 +1099,9 @@
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
+lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))"
+  by (auto simp: disjnt_def)
+
 lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
   by (auto intro!: SUP_eqI)
 
@@ -1158,6 +1161,9 @@
 lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
   by (fact SUP_constant)
 
+lemma UNION_singleton_eq_range: "(\<Union>x\<in>A. {f x}) = f ` A"
+  by blast
+
 lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   by blast
 
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -360,6 +360,30 @@
   shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   using delta [OF fin, of a b, symmetric] by (auto intro: cong)
 
+lemma delta_remove:
+  assumes fS: "finite S"
+  shows "F (\<lambda>k. if k = a then b k else c k) S = (if a \<in> S then b a \<^bold>* F c (S-{a}) else F c (S-{a}))"
+proof -
+  let ?f = "(\<lambda>k. if k = a then b k else c k)"
+  show ?thesis
+  proof (cases "a \<in> S")
+    case False
+    then have "\<forall>k\<in>S. ?f k = c k" by simp
+    with False show ?thesis by simp
+  next
+    case True
+    let ?A = "S - {a}"
+    let ?B = "{a}"
+    from True have eq: "S = ?A \<union> ?B" by blast
+    have dj: "?A \<inter> ?B = {}" by simp
+    from fS have fAB: "finite ?A" "finite ?B" by auto
+    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
+      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
+    with True show ?thesis
+      using comm_monoid_set.remove comm_monoid_set_axioms fS by fastforce
+  qed
+qed
+
 lemma If_cases:
   fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   assumes fin: "finite A"
@@ -1303,11 +1327,11 @@
   by (induct A rule: infinite_finite_induct) simp_all
 
 lemma (in linordered_semidom) prod_mono:
-  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
-  by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
+  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A"
+  by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+
 
 lemma (in linordered_semidom) prod_mono_strict:
-  assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
+  assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
   shows "prod f A < prod g A"
   using assms
 proof (induct A rule: finite_induct)
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/HOL.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1398,6 +1398,12 @@
 lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
   by simp
 
+lemma all_if_distrib: "(\<forall>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<and> (\<forall>x. x\<noteq>a \<longrightarrow> Q x)"
+  by auto
+
+lemma ex_if_distrib: "(\<exists>x. if x = a then P x else Q x) \<longleftrightarrow> P a \<or> (\<exists>x. x\<noteq>a \<and> Q x)"
+  by auto
+
 text \<open>As a simplification rule, it replaces all function equalities by
   first-order equalities.\<close>
 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -185,6 +185,9 @@
 lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
   by (simp add: f_inv_into_f)
 
+lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
+  using surj_f_inv_f[of p] by (auto simp add: bij_def)
+
 lemma inv_into_injective:
   assumes eq: "inv_into A f x = inv_into A f y"
     and x: "x \<in> f`A"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -19,9 +19,6 @@
 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
   by (simp add: Fun.swap_def)
 
-lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
-  using surj_f_inv_f[of p] by (auto simp add: bij_def)
-
 lemma bij_swap_comp:
   assumes "bij p"
   shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Limits.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -646,6 +646,12 @@
   shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Sum>i\<in>I. f i x) \<longlongrightarrow> (\<Sum>i\<in>I. a i)) F"
   by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)
 
+lemma tendsto_null_sum:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 0) F"
+  shows "((\<lambda>i. sum (f i) I) \<longlongrightarrow> 0) F"
+  using tendsto_sum [of I "\<lambda>x y. f y x" "\<lambda>x. 0"] assms by simp
+
 lemma continuous_sum [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
   shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -190,15 +190,38 @@
 
 end
 
+text \<open>Translation lemmas\<close>
+
 context ab_group_add
 begin
 
-lemma surj_plus [simp]:
-  "surj (plus a)"
+lemma surj_plus [simp]: "surj (plus a)"
   by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
 
 end
 
+lemma translation_Compl:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
+  apply (auto simp: image_iff)
+  apply (rule_tac x="x - a" in bexI, auto)
+  done
+
+lemma translation_UNIV:
+  fixes a :: "'a::ab_group_add"
+  shows "range (\<lambda>x. a + x) = UNIV"
+  by (fact surj_plus)
+
+lemma translation_diff:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
+  by auto
+
+lemma translation_Int:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
+  by auto
+
 context semidom_divide
 begin
 
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Orderings.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -727,6 +727,9 @@
   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
 
+  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3ALL _~=_./ _)"  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3EX _~=_./ _)"  [0, 0, 10] 10)
+
 syntax
   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
@@ -738,11 +741,16 @@
   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
 
+  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<noteq>_./ _)"  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<noteq>_./ _)"  [0, 0, 10] 10)
+
 syntax (input)
   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
+  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3! _~=_./ _)"  [0, 0, 10] 10)
+  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3? _~=_./ _)"  [0, 0, 10] 10)
 
 translations
   "\<forall>x<y. P" \<rightharpoonup> "\<forall>x. x < y \<longrightarrow> P"
@@ -753,6 +761,8 @@
   "\<exists>x>y. P" \<rightharpoonup> "\<exists>x. x > y \<and> P"
   "\<forall>x\<ge>y. P" \<rightharpoonup> "\<forall>x. x \<ge> y \<longrightarrow> P"
   "\<exists>x\<ge>y. P" \<rightharpoonup> "\<exists>x. x \<ge> y \<and> P"
+  "\<forall>x\<noteq>y. P" \<rightharpoonup> "\<forall>x. x \<noteq> y \<longrightarrow> P"
+  "\<exists>x\<noteq>y. P" \<rightharpoonup> "\<exists>x. x \<noteq> y \<and> P"
 
 print_translation \<open>
 let
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1849,6 +1849,27 @@
   for L :: "'a::metric_space"
   by (simp add: lim_sequentially)
 
+lemma LIMSEQ_norm_0:
+  assumes  "\<And>n::nat. norm (f n) < 1 / real (Suc n)"
+  shows "f \<longlonglongrightarrow> 0"
+proof (rule metric_LIMSEQ_I)
+  fix \<epsilon> :: "real"
+  assume "\<epsilon> > 0"
+  then obtain N::nat where "\<epsilon> > inverse N" "N > 0"
+    by (metis neq0_conv real_arch_inverse)
+  then have "norm (f n) < \<epsilon>" if "n \<ge> N" for n
+  proof -
+    have "1 / (Suc n) \<le> 1 / N"
+      using \<open>0 < N\<close> inverse_of_nat_le le_SucI that by blast
+    also have "\<dots> < \<epsilon>"
+      by (metis (no_types) \<open>inverse (real N) < \<epsilon>\<close> inverse_eq_divide)
+    finally show ?thesis
+      by (meson assms less_eq_real_def not_le order_trans)
+  qed
+  then show "\<exists>no. \<forall>n\<ge>no. dist (f n) 0 < \<epsilon>"
+    by auto
+qed
+
 
 subsubsection \<open>Limits of Functions\<close>
 
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Set.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1849,7 +1849,7 @@
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
-lemma pairwiseI:
+lemma pairwiseI [intro?]:
   "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   using that by (simp add: pairwise_def)
 
@@ -1871,8 +1871,8 @@
 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
   by (force simp: pairwise_def)
 
-lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
-  by (auto simp: pairwise_def)
+lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y; B \<subseteq> A\<rbrakk> \<Longrightarrow> pairwise Q B"
+  by (fastforce simp: pairwise_def)
 
 lemma pairwise_imageI:
   "pairwise P (f ` A)"
diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Zorn.thy
--- a/src/HOL/Zorn.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Zorn.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -469,6 +469,12 @@
   shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
   using assms Chains_subset Chains_subset' by blast
 
+lemma pairwise_chain_Union:
+  assumes P: "\<And>S. S \<in> \<C> \<Longrightarrow> pairwise R S" and "chain\<^sub>\<subseteq> \<C>"
+  shows "pairwise R (\<Union>\<C>)"
+  using \<open>chain\<^sub>\<subseteq> \<C>\<close> unfolding pairwise_def chain_subset_def
+  by (blast intro: P [unfolded pairwise_def, rule_format])
+
 lemma Zorn_Lemma: "\<forall>C\<in>chains A. \<Union>C \<in> A \<Longrightarrow> \<exists>M\<in>A. \<forall>X\<in>A. M \<subseteq> X \<longrightarrow> X = M"
   using subset_Zorn' [of A] by (force simp: chains_alt_def)