--- 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"
--- 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
--- 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)"
--- 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])
--- 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
--- 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>
--- 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
--- 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"
--- 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
--- 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)
--- 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)"
--- 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"
--- 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"
--- 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)"
--- 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
--- 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
--- 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>
--- 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)"
--- 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)