# HG changeset patch
# User nipkow
# Date 1525969075 -7200
# Node ID 53b4e204755e22ce367db1326beaefeebfefea4b
# Parent  c738f40e88d493959787a2cd863f0ba5b453b578# Parent  b105964ae3c4f99f787e34d167ccc8cc4329a42a
merged

diff -r b105964ae3c4 -r 53b4e204755e src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Thu May 10 18:17:43 2018 +0200
+++ b/src/HOL/Analysis/Determinants.thy	Thu May 10 18:17:55 2018 +0200
@@ -77,7 +77,7 @@
   }
   then show ?thesis
     unfolding det_def
-    by (subst sum_permutations_inverse) (blast intro: sum.cong elim: )
+    by (subst sum_permutations_inverse) (blast intro: sum.cong)
 qed
 
 lemma det_lowerdiagonal:
@@ -91,7 +91,7 @@
   have fU: "finite ?U"
     by simp
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
   proof
     fix p
@@ -118,7 +118,7 @@
   have fU: "finite ?U"
     by simp
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
   proof
     fix p
@@ -145,7 +145,7 @@
   have fU: "finite ?U" by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
   proof
     fix p
@@ -250,8 +250,8 @@
     have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x"
       by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq
           permutation_permutes permutation_swap_id sign_compose x)
-    also have "... = - sign x" using sign_tjk by simp
-    also have "... \<noteq> sign x" unfolding sign_def by simp
+    also have "\<dots> = - sign x" using sign_tjk by simp
+    also have "\<dots> \<noteq> sign x" unfolding sign_def by simp
     finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2"
       using x by force+
   }
@@ -274,9 +274,9 @@
   have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
   \<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}"
     unfolding g_S1 by (rule sum.reindex[OF inj_g])
-  also have "... = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
-    unfolding o_def by (rule sum.cong, auto simp add: tjk_eq)
-  also have "... = sum (\<lambda>p. - ?f p) ?S1"
+  also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
+    unfolding o_def by (rule sum.cong, auto simp: tjk_eq)
+  also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1"
   proof (rule sum.cong, auto)
     fix x assume x: "x permutes ?U"
       and even_x: "evenperm x"
@@ -289,14 +289,14 @@
       = - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))"
       by auto
   qed
-  also have "...= - sum ?f ?S1" unfolding sum_negf ..
+  also have "\<dots>= - sum ?f ?S1" unfolding sum_negf ..
   finally have *: "sum ?f ?S2 = - sum ?f ?S1" .
   have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))"
     unfolding det_def ..
-  also have "...= sum ?f ?S1 + sum ?f ?S2"
+  also have "\<dots>= sum ?f ?S1 + sum ?f ?S2"
     by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto)
-  also have "...= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
-  also have "...= 0" by simp
+  also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
+  also have "\<dots>= 0" by simp
   finally show "det A = 0" by simp
 qed
 
@@ -309,7 +309,7 @@
 lemma det_zero_row:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
-  by (force simp add: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
+  by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
 
 lemma det_zero_column:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
@@ -376,7 +376,7 @@
   have kU: "?U = insert k ?Uk"
     by blast
   have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
-    by (auto simp: )
+    by auto
   have Uk: "finite ?Uk" "k \<notin> ?Uk"
     by auto
   have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
@@ -475,7 +475,7 @@
   proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A")
     case True
     with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}"
-      by (auto simp add: rows_def intro!: vec.span_mono)
+      by (auto simp: rows_def intro!: vec.span_mono)
     then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}"
       by (meson i subsetCE vec.span_neg)
     from det_row_span[OF this]
@@ -515,17 +515,16 @@
   have *: "{f. \<forall>i. f i = i} = {id}"
     by auto
   show ?case
-    by (auto simp add: *)
+    by (auto simp: *)
 next
   case (Suc k)
   let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
   let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})"
   have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}"
-    apply (auto simp add: image_iff)
+    apply (auto simp: image_iff)
     apply (rename_tac f)
     apply (rule_tac x="f (Suc k)" in bexI)
-    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI)
-    apply auto
+    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto)
     done
   with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
   show ?case
@@ -736,7 +735,7 @@
     by blast
   have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
     unfolding sum_cmul  using c ci   
-    by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
+    by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
   have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
     unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum)
   let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
@@ -789,7 +788,7 @@
   show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
   proof (intro exI conjI)
     show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
-      by (simp add:)
+      by simp
     show "(( *v) B) \<circ> f = id"
       unfolding o_def
       by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
@@ -817,7 +816,7 @@
   show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
   proof (intro exI conjI)
     show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
-      by (simp add: )
+      by simp
     show "f \<circ> ( *v) B = id"
       using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
       by (metis (no_types, hide_lams))
@@ -967,7 +966,7 @@
 
 lemma orthogonal_transformation_compose:
    "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
-  by (auto simp add: orthogonal_transformation_def linear_compose)
+  by (auto simp: orthogonal_transformation_def linear_compose)
 
 lemma orthogonal_transformation_neg:
   "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
@@ -1018,8 +1017,7 @@
   using oA oB
   unfolding orthogonal_matrix matrix_transpose_mul
   apply (subst matrix_mul_assoc)
-  apply (subst matrix_mul_assoc[symmetric])
-  apply (simp add: )
+  apply (subst matrix_mul_assoc[symmetric], simp)
   done
 
 lemma orthogonal_transformation_matrix:
@@ -1081,8 +1079,7 @@
     have th0: "x * x - 1 = (x - 1) * (x + 1)"
       by (simp add: field_simps)
     have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
-      apply (subst eq_iff_diff_eq_0)
-      apply simp
+      apply (subst eq_iff_diff_eq_0, simp)
       done
     have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
       by simp
@@ -1199,7 +1196,7 @@
 proof -
   obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
    and "independent S" "card S = CARD('n)" "span S = UNIV"
-    using vector_in_orthonormal_basis assms by (force simp: )
+    using vector_in_orthonormal_basis assms by force
   then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
     by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
@@ -1349,7 +1346,7 @@
         "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
           norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
         using z
-        by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+        by (auto simp: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
       from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
         by (simp add: dist_norm)
     }
diff -r b105964ae3c4 -r 53b4e204755e src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 18:17:43 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 18:17:55 2018 +0200
@@ -75,8 +75,33 @@
 lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
   by (simp add: gen_has_prod_def)
 
+lemma gen_has_prod_eq_0:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m"
+  shows "p = 0"
+proof -
+  have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n
+    by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)
+  have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"
+    by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
+    with p show ?thesis
+      unfolding gen_has_prod_def
+    using LIMSEQ_unique by blast
+qed
+
 lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))"
   by (simp add: has_prod_def)
+      
+lemma has_prod_unique2: 
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  assumes "f has_prod a" "f has_prod b" shows "a = b"
+  using assms
+  by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)
+
+lemma has_prod_unique:
+  fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}"
+  shows "f has_prod s \<Longrightarrow> s = prodinf f"
+  by (simp add: has_prod_unique2 prodinf_def the_equality)
 
 lemma convergent_prod_altdef:
   fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
@@ -176,14 +201,14 @@
 next
   assume ?rhs then show ?lhs
     unfolding prod_defs
-    by (rule_tac x="0" in exI) (auto simp: )
+    by (rule_tac x=0 in exI) auto
 qed
 
 lemma convergent_prod_iff_convergent: 
   fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
   assumes "\<And>i. f i \<noteq> 0"
   shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
-  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
+  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
 
 
 lemma abs_convergent_prod_altdef:
@@ -385,7 +410,14 @@
     unfolding prod_defs by blast
 qed
 
-lemma abs_convergent_prod_ignore_initial_segment:
+corollary convergent_prod_ignore_nonzero_segment:
+  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+  assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
+  shows "\<exists>p. gen_has_prod f M p"
+  using convergent_prod_ignore_initial_segment [OF f]
+  by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
+
+corollary abs_convergent_prod_ignore_initial_segment:
   assumes "abs_convergent_prod f"
   shows   "abs_convergent_prod (\<lambda>n. f (n + m))"
   using assms unfolding abs_convergent_prod_def 
@@ -519,15 +551,13 @@
   with L show ?thesis by (auto simp: prod_defs)
 qed
 
-lemma convergent_prod_offset_0:
+lemma gen_has_prod_cases:
   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
-  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
-  shows "\<exists>p. gen_has_prod f 0 p"
-  using assms
-  unfolding convergent_prod_def
-proof (clarsimp simp: prod_defs)
-  fix M p
-  assume "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
+  assumes "gen_has_prod f M p"
+  obtains i where "i<M" "f i = 0" | p where "gen_has_prod f 0 p"
+proof -
+  have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
+    using assms unfolding gen_has_prod_def by blast+
   then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
     by (metis tendsto_mult_left)
   moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
@@ -536,17 +566,24 @@
       by auto
     then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
       by simp (subst prod.union_disjoint; force)
-    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
+    also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
       by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
     finally show ?thesis by metis
   qed
   ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
     by (auto intro: LIMSEQ_offset [where k=M])
-  then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
-    using \<open>p \<noteq> 0\<close> assms
-    by (rule_tac x="prod f {..<M} * p" in exI) auto
+  then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
+    using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def)
+  then show thesis
+    using that by blast
 qed
 
+corollary convergent_prod_offset_0:
+  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
+  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
+  shows "\<exists>p. gen_has_prod f 0 p"
+  using assms convergent_prod_def gen_has_prod_cases by blast
+
 lemma prodinf_eq_lim:
   fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
@@ -579,7 +616,7 @@
     case (elim n)
     then have "{..n} = {..<N} \<union> {N..n}"
       by auto
-    also have "prod f ... = prod f {..<N} * prod f {N..n}"
+    also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"
       by (intro prod.union_disjoint) auto
     also from N have "prod f {N..n} = prod g {N..n}"
       by (intro prod.cong) simp_all
@@ -619,7 +656,7 @@
   have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
   proof (rule prod.mono_neutral_right)
     show "N \<subseteq> {..n + Suc (Max N)}"
-      by (auto simp add: le_Suc_eq trans_le_add2)
+      by (auto simp: le_Suc_eq trans_le_add2)
     show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
       using f by blast
   qed auto
@@ -650,7 +687,7 @@
         show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
           using le_Suc_ex by fastforce
       qed (auto simp: inj_on_def)
-      also have "... = ?q"
+      also have "\<dots> = ?q"
         by (rule prod.mono_neutral_right)
            (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
       finally show ?thesis .
@@ -714,5 +751,71 @@
   shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
   using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
 
+context
+  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
+begin
+
+lemma convergent_prod_imp_has_prod: 
+  assumes "convergent_prod f"
+  shows "\<exists>p. f has_prod p"
+proof -
+  obtain M p where p: "gen_has_prod f M p"
+    using assms convergent_prod_def by blast
+  then have "p \<noteq> 0"
+    using gen_has_prod_nonzero by blast
+  with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i
+    using gen_has_prod_eq_0 that by blast
+  define C where "C = (\<Prod>n<M. f n)"
+  show ?thesis
+  proof (cases "\<forall>n\<le>M. f n \<noteq> 0")
+    case True
+    then have "C \<noteq> 0"
+      by (simp add: C_def)
+    then show ?thesis
+      by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)
+  next
+    case False
+    let ?N = "GREATEST n. f n = 0"
+    have 0: "f ?N = 0"
+      using fnz False
+      by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
+    have "f i \<noteq> 0" if "i > ?N" for i
+      by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
+    then have "\<exists>p. gen_has_prod f (Suc ?N) p"
+      using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
+    then show ?thesis
+      unfolding has_prod_def using 0 by blast
+  qed
+qed
+
+lemma convergent_prod_has_prod [intro]:
+  shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)"
+  unfolding prodinf_def
+  by (metis convergent_prod_imp_has_prod has_prod_unique theI')
+
+lemma convergent_prod_LIMSEQ:
+  shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"
+  by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent 
+      convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
+
+lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
+proof
+  assume "f has_prod x"
+  then show "convergent_prod f \<and> prodinf f = x"
+    apply safe
+    using convergent_prod_def has_prod_def apply blast
+    using has_prod_unique by blast
+qed auto
+
+lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f"
+  by (auto simp: has_prod_iff convergent_prod_has_prod)
+
+lemma prodinf_finite:
+  assumes N: "finite N"
+    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
+  shows "prodinf f = (\<Prod>n\<in>N. f n)"
+  using has_prod_finite[OF assms, THEN has_prod_unique] by simp
 
 end
+
+end