lots of new material, ultimately related to measure theory
authorpaulson <lp15@cam.ac.uk>
Mon Feb 19 16:44:45 2018 +0000 (18 months ago)
changeset 67673c8caefb20564
parent 67655 8f4810b9d9d1
child 67674 67909bfc3923
lots of new material, ultimately related to measure theory
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Fashoda_Theorem.thy
src/HOL/Analysis/Finite_Cartesian_Product.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Complete_Lattices.thy
src/HOL/Groups_Big.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Permutations.thy
src/HOL/Limits.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set.thy
src/HOL/Zorn.thy
     1.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Feb 18 20:08:21 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Feb 19 16:44:45 2018 +0000
     1.3 @@ -52,14 +52,6 @@
     1.4  lemmas Zero_notin_Suc = zero_notin_Suc_image
     1.5  lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
     1.6  
     1.7 -lemma sum_union_disjoint':
     1.8 -  assumes "finite A"
     1.9 -    and "finite B"
    1.10 -    and "A \<inter> B = {}"
    1.11 -    and "A \<union> B = C"
    1.12 -  shows "sum g C = sum g A + sum g B"
    1.13 -  using sum.union_disjoint[OF assms(1-3)] and assms(4) by auto
    1.14 -
    1.15  lemma pointwise_minimal_pointwise_maximal:
    1.16    fixes s :: "(nat \<Rightarrow> nat) set"
    1.17    assumes "finite s"
     2.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Feb 18 20:08:21 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Mon Feb 19 16:44:45 2018 +0000
     2.3 @@ -497,7 +497,7 @@
     2.4  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
     2.5    by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
     2.6  
     2.7 -lemma matrix_mul_lid:
     2.8 +lemma matrix_mul_lid [simp]:
     2.9    fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
    2.10    shows "mat 1 ** A = A"
    2.11    apply (simp add: matrix_matrix_mult_def mat_def)
    2.12 @@ -507,7 +507,7 @@
    2.13    done
    2.14  
    2.15  
    2.16 -lemma matrix_mul_rid:
    2.17 +lemma matrix_mul_rid [simp]:
    2.18    fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
    2.19    shows "A ** mat 1 = A"
    2.20    apply (simp add: matrix_matrix_mult_def mat_def)
    2.21 @@ -529,7 +529,7 @@
    2.22    apply simp
    2.23    done
    2.24  
    2.25 -lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
    2.26 +lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
    2.27    apply (vector matrix_vector_mult_def mat_def)
    2.28    apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong)
    2.29    done
    2.30 @@ -560,18 +560,18 @@
    2.31    apply simp
    2.32    done
    2.33  
    2.34 -lemma transpose_mat: "transpose (mat n) = mat n"
    2.35 +lemma transpose_mat [simp]: "transpose (mat n) = mat n"
    2.36    by (vector transpose_def mat_def)
    2.37  
    2.38  lemma transpose_transpose: "transpose(transpose A) = A"
    2.39    by (vector transpose_def)
    2.40  
    2.41 -lemma row_transpose:
    2.42 +lemma row_transpose [simp]:
    2.43    fixes A:: "'a::semiring_1^_^_"
    2.44    shows "row i (transpose A) = column i A"
    2.45    by (simp add: row_def column_def transpose_def vec_eq_iff)
    2.46  
    2.47 -lemma column_transpose:
    2.48 +lemma column_transpose [simp]:
    2.49    fixes A:: "'a::semiring_1^_^_"
    2.50    shows "column i (transpose A) = row i A"
    2.51    by (simp add: row_def column_def transpose_def vec_eq_iff)
    2.52 @@ -582,12 +582,22 @@
    2.53  lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
    2.54    by (metis transpose_transpose rows_transpose)
    2.55  
    2.56 +lemma matrix_mult_transpose_dot_column:
    2.57 +  fixes A :: "real^'n^'n"
    2.58 +  shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
    2.59 +  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
    2.60 +
    2.61 +lemma matrix_mult_transpose_dot_row:
    2.62 +  fixes A :: "real^'n^'n"
    2.63 +  shows "A ** transpose A = (\<chi> i j. (row i A) \<bullet> (row j A))"
    2.64 +  by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
    2.65 +
    2.66  text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
    2.67  
    2.68  lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
    2.69    by (simp add: matrix_vector_mult_def inner_vec_def)
    2.70  
    2.71 -lemma matrix_mult_vsum:
    2.72 +lemma matrix_mult_sum:
    2.73    "(A::'a::comm_semiring_1^'n^'m) *v x = sum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
    2.74    by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult.commute)
    2.75  
    2.76 @@ -632,6 +642,37 @@
    2.77    by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
    2.78        field_simps sum_distrib_left sum.distrib)
    2.79  
    2.80 +lemma matrix_vector_mult_add_distrib [algebra_simps]:
    2.81 +  fixes A :: "real^'n^'m"
    2.82 +  shows "A *v (x + y) = A *v x + A *v y"
    2.83 +  using matrix_vector_mul_linear [of A]  by (simp add: linear_add)
    2.84 +
    2.85 +lemma matrix_vector_mult_diff_distrib [algebra_simps]:
    2.86 +  fixes A :: "real^'n^'m"
    2.87 +  shows "A *v (x - y) = A *v x - A *v y"
    2.88 +  using matrix_vector_mul_linear [of A]  by (simp add: linear_diff)
    2.89 +
    2.90 +lemma matrix_vector_mult_scaleR[algebra_simps]:
    2.91 +  fixes A :: "real^'n^'m"
    2.92 +  shows "A *v (c *\<^sub>R x) = c *\<^sub>R (A *v x)"
    2.93 +  using linear_iff matrix_vector_mul_linear by blast
    2.94 +
    2.95 +lemma matrix_vector_mult_0_right [simp]: "A *v 0 = 0"
    2.96 +  by (simp add: matrix_vector_mult_def vec_eq_iff)
    2.97 +
    2.98 +lemma matrix_vector_mult_0 [simp]: "0 *v w = 0"
    2.99 +  by (simp add: matrix_vector_mult_def vec_eq_iff)
   2.100 +
   2.101 +lemma matrix_vector_mult_add_rdistrib [algebra_simps]:
   2.102 +  fixes A :: "real^'n^'m"
   2.103 +  shows "(A + B) *v x = (A *v x) + (B *v x)"
   2.104 +  by (simp add: vec_eq_iff inner_add_left matrix_vector_mul_component)
   2.105 +
   2.106 +lemma matrix_vector_mult_diff_rdistrib [algebra_simps]:
   2.107 +  fixes A :: "real^'n^'m"
   2.108 +  shows "(A - B) *v x = (A *v x) - (B *v x)"
   2.109 +  by (simp add: vec_eq_iff inner_diff_left matrix_vector_mul_component)
   2.110 +
   2.111  lemma matrix_works:
   2.112    assumes lf: "linear f"
   2.113    shows "matrix f *v x = f (x::real ^ 'n)"
   2.114 @@ -641,7 +682,7 @@
   2.115  lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
   2.116    by (simp add: ext matrix_works)
   2.117  
   2.118 -lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
   2.119 +lemma matrix_of_matrix_vector_mul [simp]: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A"
   2.120    by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
   2.121  
   2.122  lemma matrix_compose:
   2.123 @@ -768,7 +809,7 @@
   2.124        let ?x = "\<chi> i. c i"
   2.125        have th0:"A *v ?x = 0"
   2.126          using c
   2.127 -        unfolding matrix_mult_vsum vec_eq_iff
   2.128 +        unfolding matrix_mult_sum vec_eq_iff
   2.129          by auto
   2.130        from k[rule_format, OF th0] i
   2.131        have "c i = 0" by (vector vec_eq_iff)}
   2.132 @@ -777,7 +818,7 @@
   2.133    { assume H: ?rhs
   2.134      { fix x assume x: "A *v x = 0"
   2.135        let ?c = "\<lambda>i. ((x$i ):: real)"
   2.136 -      from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x]
   2.137 +      from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
   2.138        have "x = 0" by vector }
   2.139    }
   2.140    ultimately show ?thesis unfolding matrix_left_invertible_ker by blast
   2.141 @@ -798,7 +839,7 @@
   2.142    let ?U = "UNIV :: 'm set"
   2.143    have fU: "finite ?U" by simp
   2.144    have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
   2.145 -    unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def
   2.146 +    unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
   2.147      apply (subst eq_commute)
   2.148      apply rule
   2.149      done
   2.150 @@ -1002,7 +1043,7 @@
   2.151      and "cbox a b = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
   2.152    by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_box Basis_vec_def inner_axis)
   2.153  
   2.154 -lemma mem_interval_cart:
   2.155 +lemma mem_box_cart:
   2.156    fixes a :: "real^'n"
   2.157    shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
   2.158      and "x \<in> cbox a b \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
   2.159 @@ -1014,7 +1055,7 @@
   2.160      and "(cbox a b = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
   2.161  proof -
   2.162    { fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b"
   2.163 -    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto
   2.164 +    hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_box_cart by auto
   2.165      hence "a$i < b$i" by auto
   2.166      hence False using as by auto }
   2.167    moreover
   2.168 @@ -1025,11 +1066,11 @@
   2.169        hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
   2.170          unfolding vector_smult_component and vector_add_component
   2.171          by auto }
   2.172 -    hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto }
   2.173 +    hence "box a b \<noteq> {}" using mem_box_cart(1)[of "?x" a b] by auto }
   2.174    ultimately show ?th1 by blast
   2.175  
   2.176    { fix i x assume as:"b$i < a$i" and x:"x\<in>cbox a b"
   2.177 -    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval_cart by auto
   2.178 +    hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_box_cart by auto
   2.179      hence "a$i \<le> b$i" by auto
   2.180      hence False using as by auto }
   2.181    moreover
   2.182 @@ -1040,7 +1081,7 @@
   2.183        hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
   2.184          unfolding vector_smult_component and vector_add_component
   2.185          by auto }
   2.186 -    hence "cbox a b \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto  }
   2.187 +    hence "cbox a b \<noteq> {}" using mem_box_cart(2)[of "?x" a b] by auto  }
   2.188    ultimately show ?th2 by blast
   2.189  qed
   2.190  
   2.191 @@ -1057,7 +1098,7 @@
   2.192      and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> cbox c d \<subseteq> box a b"
   2.193      and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> cbox a b"
   2.194      and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b"
   2.195 -  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart
   2.196 +  unfolding subset_eq[unfolded Ball_def] unfolding mem_box_cart
   2.197    by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
   2.198  
   2.199  lemma interval_sing:
   2.200 @@ -1410,7 +1451,7 @@
   2.201    "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
   2.202    "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
   2.203    apply (rule_tac[!] set_eqI)
   2.204 -  unfolding Int_iff mem_interval_cart mem_Collect_eq interval_cbox_cart
   2.205 +  unfolding Int_iff mem_box_cart mem_Collect_eq interval_cbox_cart
   2.206    unfolding vec_lambda_beta
   2.207    by auto
   2.208  
     3.1 --- a/src/HOL/Analysis/Connected.thy	Sun Feb 18 20:08:21 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Feb 19 16:44:45 2018 +0000
     3.3 @@ -3016,28 +3016,6 @@
     3.4      using compact_closed_sums[OF compact_sing[of a] assms] by auto
     3.5  qed
     3.6  
     3.7 -lemma translation_Compl:
     3.8 -  fixes a :: "'a::ab_group_add"
     3.9 -  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
    3.10 -  apply (auto simp: image_iff)
    3.11 -  apply (rule_tac x="x - a" in bexI, auto)
    3.12 -  done
    3.13 -
    3.14 -lemma translation_UNIV:
    3.15 -  fixes a :: "'a::ab_group_add"
    3.16 -  shows "range (\<lambda>x. a + x) = UNIV"
    3.17 -  by (fact surj_plus)
    3.18 -
    3.19 -lemma translation_diff:
    3.20 -  fixes a :: "'a::ab_group_add"
    3.21 -  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
    3.22 -  by auto
    3.23 -
    3.24 -lemma translation_Int:
    3.25 -  fixes a :: "'a::ab_group_add"
    3.26 -  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
    3.27 -  by auto
    3.28 -
    3.29  lemma closure_translation:
    3.30    fixes a :: "'a::real_normed_vector"
    3.31    shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
     4.1 --- a/src/HOL/Analysis/Determinants.thy	Sun Feb 18 20:08:21 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Determinants.thy	Mon Feb 19 16:44:45 2018 +0000
     4.3 @@ -54,7 +54,7 @@
     4.4  
     4.5  text \<open>Basic determinant properties.\<close>
     4.6  
     4.7 -lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
     4.8 +lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
     4.9  proof -
    4.10    let ?di = "\<lambda>A i j. A$i$j"
    4.11    let ?U = "(UNIV :: 'n set)"
    4.12 @@ -193,33 +193,10 @@
    4.13      unfolding det_def by (simp add: sign_id)
    4.14  qed
    4.15  
    4.16 -lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
    4.17 -proof -
    4.18 -  let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
    4.19 -  let ?U = "UNIV :: 'n set"
    4.20 -  let ?f = "\<lambda>i j. ?A$i$j"
    4.21 -  {
    4.22 -    fix i
    4.23 -    assume i: "i \<in> ?U"
    4.24 -    have "?f i i = 1"
    4.25 -      using i by (vector mat_def)
    4.26 -  }
    4.27 -  then have th: "prod (\<lambda>i. ?f i i) ?U = prod (\<lambda>x. 1) ?U"
    4.28 -    by (auto intro: prod.cong)
    4.29 -  {
    4.30 -    fix i j
    4.31 -    assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
    4.32 -    have "?f i j = 0" using i j ij
    4.33 -      by (vector mat_def)
    4.34 -  }
    4.35 -  then have "det ?A = prod (\<lambda>i. ?f i i) ?U"
    4.36 -    using det_diagonal by blast
    4.37 -  also have "\<dots> = 1"
    4.38 -    unfolding th prod.neutral_const ..
    4.39 -  finally show ?thesis .
    4.40 -qed
    4.41 +lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
    4.42 +  by (simp add: det_diagonal mat_def)
    4.43  
    4.44 -lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
    4.45 +lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
    4.46    by (simp add: det_def prod_zero)
    4.47  
    4.48  lemma det_permute_rows:
    4.49 @@ -487,6 +464,21 @@
    4.50      done
    4.51  qed
    4.52  
    4.53 +lemma matrix_id_mat_1: "matrix id = mat 1"
    4.54 +  by (simp add: mat_def matrix_def axis_def)
    4.55 +
    4.56 +lemma matrix_id [simp]: "det (matrix id) = 1"
    4.57 +  by (simp add: matrix_id_mat_1)
    4.58 +
    4.59 +lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
    4.60 +  by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
    4.61 +
    4.62 +lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)"
    4.63 +  apply (subst det_diagonal)
    4.64 +   apply (auto simp: matrix_def mat_def prod_constant)
    4.65 +  apply (simp add: cart_eq_inner_axis inner_axis_axis)
    4.66 +  done
    4.67 +
    4.68  text \<open>
    4.69    May as well do this, though it's a bit unsatisfactory since it ignores
    4.70    exact duplicates by considering the rows/columns as a set.
    4.71 @@ -788,7 +780,7 @@
    4.72    shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"
    4.73    by (metis invertible_def matrix_left_right_inverse)
    4.74  
    4.75 -lemma invertible_righ_inverse:
    4.76 +lemma invertible_right_inverse:
    4.77    fixes A :: "real^'n^'n"
    4.78    shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"
    4.79    by (metis invertible_def matrix_left_right_inverse)
    4.80 @@ -800,7 +792,7 @@
    4.81    {
    4.82      assume "invertible A"
    4.83      then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"
    4.84 -      unfolding invertible_righ_inverse by blast
    4.85 +      unfolding invertible_right_inverse by blast
    4.86      then have "det (A ** B) = det (mat 1 :: real ^'n^'n)"
    4.87        by simp
    4.88      then have "det A \<noteq> 0"
    4.89 @@ -815,7 +807,7 @@
    4.90      from H obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0"
    4.91        and iU: "i \<in> ?U"
    4.92        and ci: "c i \<noteq> 0"
    4.93 -      unfolding invertible_righ_inverse
    4.94 +      unfolding invertible_right_inverse
    4.95        unfolding matrix_right_invertible_independent_rows
    4.96        by blast
    4.97      have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
    4.98 @@ -903,7 +895,7 @@
    4.99    have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U"
   4.100      by (auto simp add: row_transpose intro: sum.cong)
   4.101    show ?thesis
   4.102 -    unfolding matrix_mult_vsum
   4.103 +    unfolding matrix_mult_sum
   4.104      unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
   4.105      unfolding *[of "\<lambda>i. x$i"]
   4.106      apply (subst det_transpose[symmetric])
     5.1 --- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Feb 18 20:08:21 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Mon Feb 19 16:44:45 2018 +0000
     5.3 @@ -118,7 +118,7 @@
     5.4    let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
     5.5    have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}"
     5.6      apply (rule set_eqI)
     5.7 -    unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart
     5.8 +    unfolding image_iff Bex_def mem_box_cart interval_cbox_cart
     5.9      apply rule
    5.10      defer
    5.11      apply (rule_tac x="vec x" in exI)
    5.12 @@ -133,7 +133,7 @@
    5.13        unfolding image_iff ..
    5.14      then have "x \<noteq> 0"
    5.15        using as[of "w$1" "w$2"]
    5.16 -      unfolding mem_interval_cart atLeastAtMost_iff
    5.17 +      unfolding mem_box_cart atLeastAtMost_iff
    5.18        by auto
    5.19    } note x0 = this
    5.20    have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
    5.21 @@ -187,7 +187,7 @@
    5.22        unfolding *[symmetric] y o_def
    5.23        by (rule lem1[rule_format])
    5.24      then show "x \<in> cbox (-1) 1"
    5.25 -      unfolding mem_interval_cart interval_cbox_cart infnorm_2
    5.26 +      unfolding mem_box_cart interval_cbox_cart infnorm_2
    5.27        apply -
    5.28        apply rule
    5.29      proof -
    5.30 @@ -241,7 +241,7 @@
    5.31    qed
    5.32    note lem3 = this[rule_format]
    5.33    have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
    5.34 -    using x(1) unfolding mem_interval_cart by auto
    5.35 +    using x(1) unfolding mem_box_cart by auto
    5.36    then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
    5.37      unfolding right_minus_eq
    5.38      apply -
    5.39 @@ -274,7 +274,7 @@
    5.40        apply auto
    5.41        done
    5.42      ultimately show False
    5.43 -      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
    5.44 +      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
    5.45        apply (erule_tac x=1 in allE)
    5.46        apply auto
    5.47        done
    5.48 @@ -293,7 +293,7 @@
    5.49        apply auto
    5.50        done
    5.51      ultimately show False
    5.52 -      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
    5.53 +      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
    5.54        apply (erule_tac x=1 in allE)
    5.55        apply auto
    5.56        done
    5.57 @@ -312,7 +312,7 @@
    5.58        apply auto
    5.59        done
    5.60      ultimately show False
    5.61 -      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
    5.62 +      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
    5.63        apply (erule_tac x=2 in allE)
    5.64        apply auto
    5.65        done
    5.66 @@ -331,7 +331,7 @@
    5.67        apply auto
    5.68        done
    5.69      ultimately show False
    5.70 -      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
    5.71 +      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
    5.72        apply (erule_tac x=2 in allE)
    5.73        apply auto
    5.74        done
    5.75 @@ -426,7 +426,7 @@
    5.76      apply (rule pathfinish_in_path_image)
    5.77      unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
    5.78      unfolding pathstart_def
    5.79 -    apply (auto simp add: less_eq_vec_def mem_interval_cart)
    5.80 +    apply (auto simp add: less_eq_vec_def mem_box_cart)
    5.81      done
    5.82    then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
    5.83    have "z \<in> cbox a b"
    5.84 @@ -436,8 +436,8 @@
    5.85    then have "z = f 0"
    5.86      unfolding vec_eq_iff forall_2
    5.87      unfolding z(2) pathstart_def
    5.88 -    using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
    5.89 -    unfolding mem_interval_cart
    5.90 +    using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
    5.91 +    unfolding mem_box_cart
    5.92      apply (erule_tac x=1 in allE)
    5.93      using as
    5.94      apply auto
    5.95 @@ -458,7 +458,7 @@
    5.96      unfolding assms
    5.97      using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
    5.98      unfolding pathstart_def
    5.99 -    apply (auto simp add: less_eq_vec_def mem_interval_cart)
   5.100 +    apply (auto simp add: less_eq_vec_def mem_box_cart)
   5.101      done
   5.102    then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   5.103    have "z \<in> cbox a b"
   5.104 @@ -468,8 +468,8 @@
   5.105    then have "z = g 0"
   5.106      unfolding vec_eq_iff forall_2
   5.107      unfolding z(2) pathstart_def
   5.108 -    using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
   5.109 -    unfolding mem_interval_cart
   5.110 +    using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
   5.111 +    unfolding mem_box_cart
   5.112      apply (erule_tac x=2 in allE)
   5.113      using as
   5.114      apply auto
   5.115 @@ -745,7 +745,7 @@
   5.116      using pathstart_in_path_image pathfinish_in_path_image
   5.117      using assms(3-4)
   5.118      by auto
   5.119 -  note startfin = this[unfolded mem_interval_cart forall_2]
   5.120 +  note startfin = this[unfolded mem_box_cart forall_2]
   5.121    let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
   5.122       linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
   5.123       linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
   5.124 @@ -791,7 +791,7 @@
   5.125        apply (rule Un_least)+
   5.126        defer 3
   5.127        apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
   5.128 -      unfolding mem_interval_cart forall_2 vector_2
   5.129 +      unfolding mem_box_cart forall_2 vector_2
   5.130        using ab startfin abab assms(3)
   5.131        using assms(9-)
   5.132        unfolding assms
   5.133 @@ -803,7 +803,7 @@
   5.134        apply (rule Un_least)+
   5.135        defer 2
   5.136        apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
   5.137 -      unfolding mem_interval_cart forall_2 vector_2
   5.138 +      unfolding mem_box_cart forall_2 vector_2
   5.139        using ab startfin abab assms(4)
   5.140        using assms(9-)
   5.141        unfolding assms
   5.142 @@ -833,7 +833,7 @@
   5.143        have "pathfinish f \<in> cbox a b"
   5.144          using assms(3) pathfinish_in_path_image[of f] by auto
   5.145        then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
   5.146 -        unfolding mem_interval_cart forall_2 by auto
   5.147 +        unfolding mem_box_cart forall_2 by auto
   5.148        then have "z$1 \<noteq> pathfinish f$1"
   5.149          using prems(2)
   5.150          using assms ab
   5.151 @@ -842,7 +842,7 @@
   5.152          using assms(3) pathstart_in_path_image[of f]
   5.153          by auto
   5.154        then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
   5.155 -        unfolding mem_interval_cart forall_2
   5.156 +        unfolding mem_box_cart forall_2
   5.157          by auto
   5.158        then have "z$1 \<noteq> pathstart f$1"
   5.159          using prems(2) using assms ab
   5.160 @@ -857,7 +857,7 @@
   5.161        moreover have "pathstart g \<in> cbox a b"
   5.162          using assms(4) pathstart_in_path_image[of g]
   5.163          by auto
   5.164 -      note this[unfolded mem_interval_cart forall_2]
   5.165 +      note this[unfolded mem_box_cart forall_2]
   5.166        then have "z$1 \<noteq> pathstart g$1"
   5.167          using prems(1)
   5.168          using assms ab
   5.169 @@ -880,7 +880,7 @@
   5.170        by auto
   5.171      with z' show "z \<in> path_image f"
   5.172        using z(1)
   5.173 -      unfolding Un_iff mem_interval_cart forall_2
   5.174 +      unfolding Un_iff mem_box_cart forall_2
   5.175        apply -
   5.176        apply (simp only: segment_vertical segment_horizontal vector_2)
   5.177        unfolding assms
   5.178 @@ -892,7 +892,7 @@
   5.179        by auto
   5.180      with z' show "z \<in> path_image g"
   5.181        using z(2)
   5.182 -      unfolding Un_iff mem_interval_cart forall_2
   5.183 +      unfolding Un_iff mem_box_cart forall_2
   5.184        apply (simp only: segment_vertical segment_horizontal vector_2)
   5.185        unfolding assms
   5.186        apply auto
     6.1 --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Feb 18 20:08:21 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Feb 19 16:44:45 2018 +0000
     6.3 @@ -18,6 +18,8 @@
     6.4  typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
     6.5    morphisms vec_nth vec_lambda ..
     6.6  
     6.7 +declare vec_lambda_inject [simplified, simp]
     6.8 +
     6.9  notation
    6.10    vec_nth (infixl "$" 90) and
    6.11    vec_lambda (binder "\<chi>" 10)
    6.12 @@ -54,7 +56,7 @@
    6.13  lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f"
    6.14    by (auto simp add: vec_eq_iff)
    6.15  
    6.16 -lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g"
    6.17 +lemma vec_lambda_eta [simp]: "(\<chi> i. (g$i)) = g"
    6.18    by (simp add: vec_eq_iff)
    6.19  
    6.20  subsection \<open>Cardinality of vectors\<close>
     7.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Feb 18 20:08:21 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Feb 19 16:44:45 2018 +0000
     7.3 @@ -1134,4 +1134,12 @@
     7.4    qed
     7.5  qed
     7.6  
     7.7 +lemma lebesgue_openin:
     7.8 +   "\<lbrakk>openin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
     7.9 +  by (metis borel_open openin_open sets.Int sets_completionI_sets sets_lborel)
    7.10 +
    7.11 +lemma lebesgue_closedin:
    7.12 +   "\<lbrakk>closedin (subtopology euclidean S) T; S \<in> sets lebesgue\<rbrakk> \<Longrightarrow> T \<in> sets lebesgue"
    7.13 +  by (metis borel_closed closedin_closed sets.Int sets_completionI_sets sets_lborel)
    7.14 +
    7.15  end
     8.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Feb 18 20:08:21 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Mon Feb 19 16:44:45 2018 +0000
     8.3 @@ -1749,6 +1749,10 @@
     8.4  lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
     8.5    using fmeasurableI2[of A M "A - B"] by auto
     8.6  
     8.7 +lemma fmeasurable_Int_fmeasurable:
     8.8 +   "\<lbrakk>S \<in> fmeasurable M; T \<in> sets M\<rbrakk> \<Longrightarrow> (S \<inter> T) \<in> fmeasurable M"
     8.9 +  by (meson fmeasurableD fmeasurableI2 inf_le1 sets.Int)
    8.10 +
    8.11  lemma fmeasurable_UN:
    8.12    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"
    8.13    shows "(\<Union>i\<in>I. F i) \<in> fmeasurable M"
     9.1 --- a/src/HOL/Complete_Lattices.thy	Sun Feb 18 20:08:21 2018 +0100
     9.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Feb 19 16:44:45 2018 +0000
     9.3 @@ -1099,6 +1099,9 @@
     9.4    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
     9.5  \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
     9.6  
     9.7 +lemma disjoint_UN_iff: "disjnt A (\<Union>i\<in>I. B i) \<longleftrightarrow> (\<forall>i\<in>I. disjnt A (B i))"
     9.8 +  by (auto simp: disjnt_def)
     9.9 +
    9.10  lemma UNION_eq: "(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
    9.11    by (auto intro!: SUP_eqI)
    9.12  
    9.13 @@ -1158,6 +1161,9 @@
    9.14  lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
    9.15    by (fact SUP_constant)
    9.16  
    9.17 +lemma UNION_singleton_eq_range: "(\<Union>x\<in>A. {f x}) = f ` A"
    9.18 +  by blast
    9.19 +
    9.20  lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
    9.21    by blast
    9.22  
    10.1 --- a/src/HOL/Groups_Big.thy	Sun Feb 18 20:08:21 2018 +0100
    10.2 +++ b/src/HOL/Groups_Big.thy	Mon Feb 19 16:44:45 2018 +0000
    10.3 @@ -360,6 +360,30 @@
    10.4    shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
    10.5    using delta [OF fin, of a b, symmetric] by (auto intro: cong)
    10.6  
    10.7 +lemma delta_remove:
    10.8 +  assumes fS: "finite S"
    10.9 +  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}))"
   10.10 +proof -
   10.11 +  let ?f = "(\<lambda>k. if k = a then b k else c k)"
   10.12 +  show ?thesis
   10.13 +  proof (cases "a \<in> S")
   10.14 +    case False
   10.15 +    then have "\<forall>k\<in>S. ?f k = c k" by simp
   10.16 +    with False show ?thesis by simp
   10.17 +  next
   10.18 +    case True
   10.19 +    let ?A = "S - {a}"
   10.20 +    let ?B = "{a}"
   10.21 +    from True have eq: "S = ?A \<union> ?B" by blast
   10.22 +    have dj: "?A \<inter> ?B = {}" by simp
   10.23 +    from fS have fAB: "finite ?A" "finite ?B" by auto
   10.24 +    have "F ?f S = F ?f ?A \<^bold>* F ?f ?B"
   10.25 +      using union_disjoint [OF fAB dj, of ?f, unfolded eq [symmetric]] by simp
   10.26 +    with True show ?thesis
   10.27 +      using comm_monoid_set.remove comm_monoid_set_axioms fS by fastforce
   10.28 +  qed
   10.29 +qed
   10.30 +
   10.31  lemma If_cases:
   10.32    fixes P :: "'b \<Rightarrow> bool" and g h :: "'b \<Rightarrow> 'a"
   10.33    assumes fin: "finite A"
   10.34 @@ -1303,11 +1327,11 @@
   10.35    by (induct A rule: infinite_finite_induct) simp_all
   10.36  
   10.37  lemma (in linordered_semidom) prod_mono:
   10.38 -  "\<forall>i\<in>A. 0 \<le> f i \<and> f i \<le> g i \<Longrightarrow> prod f A \<le> prod g A"
   10.39 -  by (induct A rule: infinite_finite_induct) (auto intro!: prod_nonneg mult_mono)
   10.40 +  "(\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i \<le> g i) \<Longrightarrow> prod f A \<le> prod g A"
   10.41 +  by (induct A rule: infinite_finite_induct) (force intro!: prod_nonneg mult_mono)+
   10.42  
   10.43  lemma (in linordered_semidom) prod_mono_strict:
   10.44 -  assumes "finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
   10.45 +  assumes "finite A" "\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
   10.46    shows "prod f A < prod g A"
   10.47    using assms
   10.48  proof (induct A rule: finite_induct)
    11.1 --- a/src/HOL/HOL.thy	Sun Feb 18 20:08:21 2018 +0100
    11.2 +++ b/src/HOL/HOL.thy	Mon Feb 19 16:44:45 2018 +0000
    11.3 @@ -1398,6 +1398,12 @@
    11.4  lemma if_distrib: "f (if c then x else y) = (if c then f x else f y)"
    11.5    by simp
    11.6  
    11.7 +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)"
    11.8 +  by auto
    11.9 +
   11.10 +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)"
   11.11 +  by auto
   11.12 +
   11.13  text \<open>As a simplification rule, it replaces all function equalities by
   11.14    first-order equalities.\<close>
   11.15  lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
    12.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Feb 18 20:08:21 2018 +0100
    12.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Feb 19 16:44:45 2018 +0000
    12.3 @@ -185,6 +185,9 @@
    12.4  lemma surj_f_inv_f: "surj f \<Longrightarrow> f (inv f y) = y"
    12.5    by (simp add: f_inv_into_f)
    12.6  
    12.7 +lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
    12.8 +  using surj_f_inv_f[of p] by (auto simp add: bij_def)
    12.9 +
   12.10  lemma inv_into_injective:
   12.11    assumes eq: "inv_into A f x = inv_into A f y"
   12.12      and x: "x \<in> f`A"
    13.1 --- a/src/HOL/Library/Permutations.thy	Sun Feb 18 20:08:21 2018 +0100
    13.2 +++ b/src/HOL/Library/Permutations.thy	Mon Feb 19 16:44:45 2018 +0000
    13.3 @@ -19,9 +19,6 @@
    13.4  lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    13.5    by (simp add: Fun.swap_def)
    13.6  
    13.7 -lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
    13.8 -  using surj_f_inv_f[of p] by (auto simp add: bij_def)
    13.9 -
   13.10  lemma bij_swap_comp:
   13.11    assumes "bij p"
   13.12    shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
    14.1 --- a/src/HOL/Limits.thy	Sun Feb 18 20:08:21 2018 +0100
    14.2 +++ b/src/HOL/Limits.thy	Mon Feb 19 16:44:45 2018 +0000
    14.3 @@ -646,6 +646,12 @@
    14.4    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"
    14.5    by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_add)
    14.6  
    14.7 +lemma tendsto_null_sum:
    14.8 +  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_add"
    14.9 +  assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 0) F"
   14.10 +  shows "((\<lambda>i. sum (f i) I) \<longlongrightarrow> 0) F"
   14.11 +  using tendsto_sum [of I "\<lambda>x y. f y x" "\<lambda>x. 0"] assms by simp
   14.12 +
   14.13  lemma continuous_sum [continuous_intros]:
   14.14    fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_add"
   14.15    shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
    15.1 --- a/src/HOL/Nat.thy	Sun Feb 18 20:08:21 2018 +0100
    15.2 +++ b/src/HOL/Nat.thy	Mon Feb 19 16:44:45 2018 +0000
    15.3 @@ -190,15 +190,38 @@
    15.4  
    15.5  end
    15.6  
    15.7 +text \<open>Translation lemmas\<close>
    15.8 +
    15.9  context ab_group_add
   15.10  begin
   15.11  
   15.12 -lemma surj_plus [simp]:
   15.13 -  "surj (plus a)"
   15.14 +lemma surj_plus [simp]: "surj (plus a)"
   15.15    by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
   15.16  
   15.17  end
   15.18  
   15.19 +lemma translation_Compl:
   15.20 +  fixes a :: "'a::ab_group_add"
   15.21 +  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
   15.22 +  apply (auto simp: image_iff)
   15.23 +  apply (rule_tac x="x - a" in bexI, auto)
   15.24 +  done
   15.25 +
   15.26 +lemma translation_UNIV:
   15.27 +  fixes a :: "'a::ab_group_add"
   15.28 +  shows "range (\<lambda>x. a + x) = UNIV"
   15.29 +  by (fact surj_plus)
   15.30 +
   15.31 +lemma translation_diff:
   15.32 +  fixes a :: "'a::ab_group_add"
   15.33 +  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
   15.34 +  by auto
   15.35 +
   15.36 +lemma translation_Int:
   15.37 +  fixes a :: "'a::ab_group_add"
   15.38 +  shows "(\<lambda>x. a + x) ` (s \<inter> t) = ((\<lambda>x. a + x) ` s) \<inter> ((\<lambda>x. a + x) ` t)"
   15.39 +  by auto
   15.40 +
   15.41  context semidom_divide
   15.42  begin
   15.43  
    16.1 --- a/src/HOL/Orderings.thy	Sun Feb 18 20:08:21 2018 +0100
    16.2 +++ b/src/HOL/Orderings.thy	Mon Feb 19 16:44:45 2018 +0000
    16.3 @@ -727,6 +727,9 @@
    16.4    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
    16.5    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
    16.6  
    16.7 +  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3ALL _~=_./ _)"  [0, 0, 10] 10)
    16.8 +  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3EX _~=_./ _)"  [0, 0, 10] 10)
    16.9 +
   16.10  syntax
   16.11    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   16.12    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   16.13 @@ -738,11 +741,16 @@
   16.14    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
   16.15    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
   16.16  
   16.17 +  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<noteq>_./ _)"  [0, 0, 10] 10)
   16.18 +  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_\<noteq>_./ _)"  [0, 0, 10] 10)
   16.19 +
   16.20  syntax (input)
   16.21    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3! _<_./ _)"  [0, 0, 10] 10)
   16.22    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3? _<_./ _)"  [0, 0, 10] 10)
   16.23    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3! _<=_./ _)" [0, 0, 10] 10)
   16.24    "_Ex_less_eq" :: "[idt, 'a, bool] => bool"    ("(3? _<=_./ _)" [0, 0, 10] 10)
   16.25 +  "_All_neq" :: "[idt, 'a, bool] => bool"    ("(3! _~=_./ _)"  [0, 0, 10] 10)
   16.26 +  "_Ex_neq" :: "[idt, 'a, bool] => bool"    ("(3? _~=_./ _)"  [0, 0, 10] 10)
   16.27  
   16.28  translations
   16.29    "\<forall>x<y. P" \<rightharpoonup> "\<forall>x. x < y \<longrightarrow> P"
   16.30 @@ -753,6 +761,8 @@
   16.31    "\<exists>x>y. P" \<rightharpoonup> "\<exists>x. x > y \<and> P"
   16.32    "\<forall>x\<ge>y. P" \<rightharpoonup> "\<forall>x. x \<ge> y \<longrightarrow> P"
   16.33    "\<exists>x\<ge>y. P" \<rightharpoonup> "\<exists>x. x \<ge> y \<and> P"
   16.34 +  "\<forall>x\<noteq>y. P" \<rightharpoonup> "\<forall>x. x \<noteq> y \<longrightarrow> P"
   16.35 +  "\<exists>x\<noteq>y. P" \<rightharpoonup> "\<exists>x. x \<noteq> y \<and> P"
   16.36  
   16.37  print_translation \<open>
   16.38  let
    17.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Feb 18 20:08:21 2018 +0100
    17.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 19 16:44:45 2018 +0000
    17.3 @@ -1849,6 +1849,27 @@
    17.4    for L :: "'a::metric_space"
    17.5    by (simp add: lim_sequentially)
    17.6  
    17.7 +lemma LIMSEQ_norm_0:
    17.8 +  assumes  "\<And>n::nat. norm (f n) < 1 / real (Suc n)"
    17.9 +  shows "f \<longlonglongrightarrow> 0"
   17.10 +proof (rule metric_LIMSEQ_I)
   17.11 +  fix \<epsilon> :: "real"
   17.12 +  assume "\<epsilon> > 0"
   17.13 +  then obtain N::nat where "\<epsilon> > inverse N" "N > 0"
   17.14 +    by (metis neq0_conv real_arch_inverse)
   17.15 +  then have "norm (f n) < \<epsilon>" if "n \<ge> N" for n
   17.16 +  proof -
   17.17 +    have "1 / (Suc n) \<le> 1 / N"
   17.18 +      using \<open>0 < N\<close> inverse_of_nat_le le_SucI that by blast
   17.19 +    also have "\<dots> < \<epsilon>"
   17.20 +      by (metis (no_types) \<open>inverse (real N) < \<epsilon>\<close> inverse_eq_divide)
   17.21 +    finally show ?thesis
   17.22 +      by (meson assms less_eq_real_def not_le order_trans)
   17.23 +  qed
   17.24 +  then show "\<exists>no. \<forall>n\<ge>no. dist (f n) 0 < \<epsilon>"
   17.25 +    by auto
   17.26 +qed
   17.27 +
   17.28  
   17.29  subsubsection \<open>Limits of Functions\<close>
   17.30  
    18.1 --- a/src/HOL/Set.thy	Sun Feb 18 20:08:21 2018 +0100
    18.2 +++ b/src/HOL/Set.thy	Mon Feb 19 16:44:45 2018 +0000
    18.3 @@ -1849,7 +1849,7 @@
    18.4  definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    18.5    where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
    18.6  
    18.7 -lemma pairwiseI:
    18.8 +lemma pairwiseI [intro?]:
    18.9    "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   18.10    using that by (simp add: pairwise_def)
   18.11  
   18.12 @@ -1871,8 +1871,8 @@
   18.13  lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
   18.14    by (force simp: pairwise_def)
   18.15  
   18.16 -lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
   18.17 -  by (auto simp: pairwise_def)
   18.18 +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"
   18.19 +  by (fastforce simp: pairwise_def)
   18.20  
   18.21  lemma pairwise_imageI:
   18.22    "pairwise P (f ` A)"
    19.1 --- a/src/HOL/Zorn.thy	Sun Feb 18 20:08:21 2018 +0100
    19.2 +++ b/src/HOL/Zorn.thy	Mon Feb 19 16:44:45 2018 +0000
    19.3 @@ -469,6 +469,12 @@
    19.4    shows "Chains r = {C. pred_on.chain UNIV (\<lambda>x y. (x, y) \<in> r) C}"
    19.5    using assms Chains_subset Chains_subset' by blast
    19.6  
    19.7 +lemma pairwise_chain_Union:
    19.8 +  assumes P: "\<And>S. S \<in> \<C> \<Longrightarrow> pairwise R S" and "chain\<^sub>\<subseteq> \<C>"
    19.9 +  shows "pairwise R (\<Union>\<C>)"
   19.10 +  using \<open>chain\<^sub>\<subseteq> \<C>\<close> unfolding pairwise_def chain_subset_def
   19.11 +  by (blast intro: P [unfolded pairwise_def, rule_format])
   19.12 +
   19.13  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"
   19.14    using subset_Zorn' [of A] by (force simp: chains_alt_def)
   19.15