diff --git a/thys/Smith_Normal_Form/Cauchy_Binet.thy b/thys/Smith_Normal_Form/Cauchy_Binet.thy --- a/thys/Smith_Normal_Form/Cauchy_Binet.thy +++ b/thys/Smith_Normal_Form/Cauchy_Binet.thy @@ -1,1426 +1,1425 @@ (* Author: Jose Divasón - Email: jose.divason@unirioja.es + Email: jose.divason@unirioja.es *) section \The Cauchy--Binet formula\ theory Cauchy_Binet imports Diagonal_To_Smith - SNF_Missing_Lemmas + SNF_Missing_Lemmas begin subsection \Previous missing results about @{text "pick"} and @{text "insert"}\ lemma pick_insert: assumes a_notin_I: "a \ I" and i2: "i < card I" and a_def: "pick (insert a I) a' = a" (*Alternative: index (insort a (sorted_list_of_set I)) a = a'*) and ia': "i < a'" (*Case 1*) and a'_card: "a' < card I + 1" shows "pick (insert a I) i = pick I i" proof - have finI: "finite I" using i2 using card_infinite by force have "pick (insert a I) i = sorted_list_of_set (insert a I) ! i" proof (rule sorted_list_of_set_eq_pick[symmetric]) have "finite (insert a I)" using card_infinite i2 by force thus "i < length (sorted_list_of_set (insert a I))" - by (metis a_notin_I card_insert_disjoint distinct_card finite_insert + by (metis a_notin_I card_insert_disjoint distinct_card finite_insert i2 less_Suc_eq sorted_list_of_set(1) sorted_list_of_set(3)) qed also have "... = insort a (sorted_list_of_set I) ! i" using sorted_list_of_set.insert by (metis a_notin_I card_infinite i2 not_less0) also have "... = (sorted_list_of_set I) ! i" proof (rule insort_nth[OF]) show "sorted (sorted_list_of_set I)" by auto show "a \ set (sorted_list_of_set I)" using a_notin_I by (metis card_infinite i2 not_less_zero set_sorted_list_of_set) have "index (sorted_list_of_set (insert a I)) a = a'" using pick_index a_def using a'_card a_notin_I finI by auto hence "index (insort a (sorted_list_of_set I)) a = a'" by (simp add: a_notin_I finI) thus "i < index (insort a (sorted_list_of_set I)) a" using ia' by auto - show "sorted_list_of_set I \ []" using finI i2 by fastforce + show "sorted_list_of_set I \ []" using finI i2 by fastforce qed also have "... = pick I i" proof (rule sorted_list_of_set_eq_pick) have "finite I" using card_infinite i2 by fastforce - thus "i < length (sorted_list_of_set I)" + thus "i < length (sorted_list_of_set I)" by (metis distinct_card distinct_sorted_list_of_set i2 set_sorted_list_of_set) qed finally show ?thesis . qed lemma pick_insert2: assumes a_notin_I: "a \ I" and i2: "i < card I" and a_def: "pick (insert a I) a' = a" (*Alternative: index (sorted_list_of_set (insert a I)) a = a'*) and ia': "i \ a'" (*Case 2*) and a'_card: "a' < card I + 1" shows "pick (insert a I) i < pick I i" proof (cases "i = 0") case True - then show ?thesis - by (auto, metis (mono_tags, lifting) DL_Missing_Sublist.pick.simps(1) Least_le a_def a_notin_I + then show ?thesis + by (auto, metis (mono_tags, lifting) DL_Missing_Sublist.pick.simps(1) Least_le a_def a_notin_I dual_order.order_iff_strict i2 ia' insertCI le_zero_eq not_less_Least pick_in_set_le) next case False hence i0: "i = Suc (i - 1)" using a'_card ia' by auto have finI: "finite I" using i2 card_infinite by force have index_a'1: "index (sorted_list_of_set (insert a I)) a = a'" using pick_index using a'_card a_def a_notin_I finI by auto - hence index_a': "index (insort a (sorted_list_of_set I)) a = a'" + hence index_a': "index (insort a (sorted_list_of_set I)) a = a'" by (simp add: a_notin_I finI) have i1_length: "i - 1 < length (sorted_list_of_set I)" using i2 - by (metis distinct_card distinct_sorted_list_of_set finI + by (metis distinct_card distinct_sorted_list_of_set finI less_imp_diff_less set_sorted_list_of_set) have 1: "pick (insert a I) i = sorted_list_of_set (insert a I) ! i" proof (rule sorted_list_of_set_eq_pick[symmetric]) have "finite (insert a I)" using card_infinite i2 by force thus "i < length (sorted_list_of_set (insert a I))" - by (metis a_notin_I card_insert_disjoint distinct_card finite_insert + by (metis a_notin_I card_insert_disjoint distinct_card finite_insert i2 less_Suc_eq sorted_list_of_set(1) sorted_list_of_set(3)) qed also have 2: "... = insort a (sorted_list_of_set I) ! i" using sorted_list_of_set.insert by (metis a_notin_I card_infinite i2 not_less0) also have "... = insort a (sorted_list_of_set I) ! Suc (i-1)" using i0 by auto also have "... < pick I i" proof (cases "i = a'") case True have "(sorted_list_of_set I) ! i > a" by (smt "1" Suc_less_eq True a_def a_notin_I distinct_card distinct_sorted_list_of_set finI i2 - ia' index_a' insort_nth2 length_insort lessI list.size(3) nat_less_le not_less_zero - pick_in_set_le set_sorted_list_of_set sorted_list_of_set(2) sorted_list_of_set.insert + ia' index_a' insort_nth2 length_insort lessI list.size(3) nat_less_le not_less_zero + pick_in_set_le set_sorted_list_of_set sorted_list_of_set(2) sorted_list_of_set.insert sorted_list_of_set_eq_pick sorted_sorted_wrt sorted_wrt_nth_less) - moreover have "a = insort a (sorted_list_of_set I) ! i" using True 1 2 a_def by auto + moreover have "a = insort a (sorted_list_of_set I) ! i" using True 1 2 a_def by auto ultimately show ?thesis using 1 2 - by (metis distinct_card finI i0 i2 set_sorted_list_of_set + by (metis distinct_card finI i0 i2 set_sorted_list_of_set sorted_list_of_set(3) sorted_list_of_set_eq_pick) next - case False + case False have "insort a (sorted_list_of_set I) ! Suc (i-1) = (sorted_list_of_set I) ! (i-1)" by (rule insort_nth2, insert i1_length False ia' index_a', auto simp add: a_notin_I finI) also have "... = pick I (i-1)" by (rule sorted_list_of_set_eq_pick[OF i1_length]) also have "... < pick I i" using i0 i2 pick_mono_le by auto finally show ?thesis . qed finally show ?thesis . qed lemma pick_insert3: assumes a_notin_I: "a \ I" and i2: "i < card I" and a_def: "pick (insert a I) a' = a" (*Alternative: index (sorted_list_of_set (insert a I)) a = a'.*) and ia': "i \ a'" (*Case 2*) and a'_card: "a' < card I + 1" shows "pick (insert a I) (Suc i) = pick I i" proof (cases "i = 0") case True have a_LEAST: "a < (LEAST aa. aa\I)" using True a_def a_notin_I i2 ia' pick_insert2 by fastforce - have Least_rw: "(LEAST aa. aa = a \ aa \ I) = a" - by (rule Least_equality, insert a_notin_I, auto, + have Least_rw: "(LEAST aa. aa = a \ aa \ I) = a" + by (rule Least_equality, insert a_notin_I, auto, metis a_LEAST le_less_trans nat_le_linear not_less_Least) let ?P = "\aa. (aa = a \ aa \ I) \ (LEAST aa. aa = a \ aa \ I) < aa" - let ?Q = "\aa. aa \ I" + let ?Q = "\aa. aa \ I" have "?P = ?Q" unfolding Least_rw fun_eq_iff - by (auto, metis a_LEAST le_less_trans not_le not_less_Least) - thus ?thesis using True by auto + by (auto, metis a_LEAST le_less_trans not_le not_less_Least) + thus ?thesis using True by auto next case False have finI: "finite I" using i2 card_infinite by force have index_a'1: "index (sorted_list_of_set (insert a I)) a = a'" using pick_index using a'_card a_def a_notin_I finI by auto - hence index_a': "index (insort a (sorted_list_of_set I)) a = a'" + hence index_a': "index (insort a (sorted_list_of_set I)) a = a'" by (simp add: a_notin_I finI) have i1_length: "i < length (sorted_list_of_set I)" using i2 by (metis distinct_card distinct_sorted_list_of_set finI set_sorted_list_of_set) have 1: "pick (insert a I) (Suc i) = sorted_list_of_set (insert a I) ! (Suc i)" proof (rule sorted_list_of_set_eq_pick[symmetric]) have "finite (insert a I)" using card_infinite i2 by force thus "Suc i < length (sorted_list_of_set (insert a I))" - by (metis Suc_mono a_notin_I card_insert_disjoint distinct_card distinct_sorted_list_of_set + by (metis Suc_mono a_notin_I card_insert_disjoint distinct_card distinct_sorted_list_of_set finI i2 set_sorted_list_of_set) qed also have 2: "... = insort a (sorted_list_of_set I) ! Suc i" using sorted_list_of_set.insert by (metis a_notin_I card_infinite i2 not_less0) also have "... = pick I i" proof (cases "i = a'") case True show ?thesis - by (metis True a_notin_I finI i1_length index_a' insort_nth2 le_refl list.size(3) not_less0 + by (metis True a_notin_I finI i1_length index_a' insort_nth2 le_refl list.size(3) not_less0 set_sorted_list_of_set sorted_list_of_set(2) sorted_list_of_set_eq_pick) next - case False + case False have "insort a (sorted_list_of_set I) ! Suc i = (sorted_list_of_set I) ! i" by (rule insort_nth2, insert i1_length False ia' index_a', auto simp add: a_notin_I finI) also have "... = pick I i" by (rule sorted_list_of_set_eq_pick[OF i1_length]) finally show ?thesis . qed finally show ?thesis . qed lemma pick_insert_index: assumes Ik: "card I = k" and a_notin_I: "a \ I" and ik: "i < k" and a_def: "pick (insert a I) a' = a" and a'k: "a' < card I + 1" shows "pick (insert a I) (insert_index a' i) = pick I i" proof (cases "i I" by (simp add: Ik ik pick_in_set_le) show "pick (insert a I) i < pick I i" by (rule pick_insert2[OF a_notin_I _ a_def _ a'k], insert False, auto simp add: Ik ik) fix y assume y: "y \ I \ pick (insert a I) i < y" let ?xs = "sorted_list_of_set (insert a I)" have "y \ set ?xs" using y by (metis fin_aI insertI2 set_sorted_list_of_set y) from this obtain j where xs_j_y: "?xs ! j = y" and j: "j < length ?xs" using in_set_conv_nth by metis have ij: "i pick (insert a I) j" - by (metis Ik Suc_lessI card_infinite distinct_card distinct_sorted_list_of_set eq_iff + also have "... \ pick (insert a I) j" + by (metis Ik Suc_lessI card_infinite distinct_card distinct_sorted_list_of_set eq_iff finite_insert ij ik j less_imp_le_nat not_less_zero pick_mono_le set_sorted_list_of_set) also have "... = ?xs ! j" by (rule sorted_list_of_set_eq_pick[symmetric, OF j]) also have "... = y" by (rule xs_j_y) finally show "pick I i \ y" . qed finally show ?thesis unfolding insert_index_def using False by auto qed subsection\Start of the proof\ definition "strict_from_inj n f = (\i. if i\{0.. nat" assumes "inj_on f {0.. {0.. {0.. f ` {0.. f ` {0.. strict_from_inj n f ` {0..)|f \. f \ {0.. {0.. (\i. i \ {0.. f i = i) +definition "Z (n::nat) (m::nat) = {(f,\)|f \. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ \ permutes {0.. {0.. {0.. (\i. i \ {0.. f i = i)} \ {\. \ permutes {0.. carrier_mat n m" and B: "B \ carrier_mat m n" - shows "det (A*B) = det (mat\<^sub>r n n (\i. finsum_vec TYPE('a::comm_ring_1) n + shows "det (A*B) = det (mat\<^sub>r n n (\i. finsum_vec TYPE('a::comm_ring_1) n (\k. B $$ (k, i) \\<^sub>v Matrix.col A k) {0..T \ carrier_mat m n" using A by auto have BT: "B\<^sup>T \ carrier_mat n m" using B by auto let ?f = "(\i. finsum_vec TYPE('a) n (\k. B\<^sup>T $$ (i, k) \\<^sub>v Matrix.row A\<^sup>T k) {0..k\{0..T $$ (i, k) \\<^sub>v row A\<^sup>T k) $ j)" + also have "... = (\k\{0..T $$ (i, k) \\<^sub>v row A\<^sup>T k) $ j)" by (rule index_finsum_vec[OF _ j_n], auto simp add: A) also have "... = (\k\{0..\<^sub>v col A k) $ j)" proof (rule sum.cong, auto) fix x assume x: "xT x = col A x" by (rule row_transpose, insert A x, auto) - have B_rw: "B\<^sup>T $$ (i,x) = B $$ (x, i)" + have B_rw: "B\<^sup>T $$ (i,x) = B $$ (x, i)" by (rule index_transpose_mat, insert x i B, auto) - have "(B\<^sup>T $$ (i, x) \\<^sub>v Matrix.row A\<^sup>T x) $v j = B\<^sup>T $$ (i, x) * Matrix.row A\<^sup>T x $v j" + have "(B\<^sup>T $$ (i, x) \\<^sub>v Matrix.row A\<^sup>T x) $v j = B\<^sup>T $$ (i, x) * Matrix.row A\<^sup>T x $v j" by (rule index_smult_vec, insert A j_n, auto) also have "... = B $$ (x, i) * col A x $v j" unfolding row_rw B_rw by simp also have "... = (B $$ (x, i) \\<^sub>v col A x) $v j" by (rule index_smult_vec[symmetric], insert A j_n, auto) finally show " (B\<^sup>T $$ (i, x) \\<^sub>v Matrix.row A\<^sup>T x) $v j = (B $$ (x, i) \\<^sub>v col A x) $v j" . - qed - also have "... = ?g i $v j" + qed + also have "... = ?g i $v j" by (rule index_finsum_vec[symmetric, OF _ j_n], auto simp add: A) also have "... = ?rhs $$ (i, j)" by (rule index_mat[symmetric], insert i j, auto) finally show "?lhs $$ (i, j) = ?rhs $$ (i, j)" . qed have "det (A*B) = det (B\<^sup>T*A\<^sup>T)" using det_transpose by (metis A B Matrix.transpose_mult mult_carrier_mat) - also have "... = det (mat\<^sub>r n n (\i. finsum_vec TYPE('a) n (\k. B\<^sup>T $$ (i, k) \\<^sub>v Matrix.row A\<^sup>T k) {0..r n n (\i. finsum_vec TYPE('a) n (\k. B\<^sup>T $$ (i, k) \\<^sub>v Matrix.row A\<^sup>T k) {0..r n n (\i. finsum_vec TYPE('a) n (\k. B $$ (k, i) \\<^sub>v Matrix.col A k) {0.. carrier_mat n m" and B: "B \ carrier_mat m n" shows "det (A*B) = (\f | (\i\{0.. {0.. (\i. i \ {0.. f i = i). (\i = 0..r n n (\i. col A (f i))))" proof - let ?V="{0..r n n (\i. B $$ (f i, i) \\<^sub>v col A (f i))) = - (prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i)))" + have det_rw: "det (mat\<^sub>r n n (\i. B $$ (f i, i) \\<^sub>v col A (f i))) = + (prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i)))" if f: "(\i\{0.. {0.. (\i. i \ {0.. f i = i)" for f - by (rule det_rows_mul, insert A col_dim, auto) + by (rule det_rows_mul, insert A col_dim, auto) have "det (A*B) = det (mat\<^sub>r n n (\i. finsum_vec TYPE('a::comm_ring_1) n (\k. B $$ (k, i) \\<^sub>v Matrix.col A k) ?U))" by (rule det_mul_finsum_alt[OF A B]) also have "... = sum ?g ?F" by (rule det_linear_rows_sum[OF fm], auto simp add: A) - also have "... = (\f\?F. prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i))))" + also have "... = (\f\?F. prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i))))" using det_rw by auto finally show ?thesis . qed lemma det_cols_mul': assumes A: "A \ carrier_mat n m" and B: "B \ carrier_mat m n" shows "det (A*B) = (\f | (\i\{0.. {0.. (\i. i \ {0.. f i = i). (\i = 0..r n n (\i. row B (f i))))" proof - let ?F="{f. (\i\{0.. {0.. (\i. i \ {0.. f i = i)}" have t: "A * B = (B\<^sup>T*A\<^sup>T)\<^sup>T" using transpose_mult[OF A B] transpose_transpose by metis - have "det (B\<^sup>T*A\<^sup>T) = (\f\?F. (\i = 0..T $$ (f i, i)) * det (mat\<^sub>r n n (\i. col B\<^sup>T (f i))))" + have "det (B\<^sup>T*A\<^sup>T) = (\f\?F. (\i = 0..T $$ (f i, i)) * det (mat\<^sub>r n n (\i. col B\<^sup>T (f i))))" by (rule det_cols_mul, auto simp add: A B) also have "... = (\f \?F. (\i = 0..r n n (\i. row B (f i))))" proof (rule sum.cong, rule refl) fix f assume f: "f \ ?F" - have "(\i = 0..T $$ (f i, i)) = (\i = 0..i = 0..T $$ (f i, i)) = (\i = 0.. {0..T $$ (f x, x) = A $$ (x, f x)" + fix x assume x: "x \ {0..T $$ (f x, x) = A $$ (x, f x)" by (rule index_transpose_mat(1), insert f A x, auto) qed moreover have "det (mat\<^sub>r n n (\i. col B\<^sup>T (f i))) = det (mat\<^sub>r n n (\i. row B (f i)))" proof - have row_eq_colT: "row B (f i) $v j = col B\<^sup>T (f i) $v j" if i: "i < n" and j: "j < n" for i j proof - have fi_m: "f i < m" using f i by auto have "col B\<^sup>T (f i) $v j = B\<^sup>T $$(j, f i)" by (rule index_col, insert B fi_m j, auto) also have "... = B $$ (f i, j)" using B fi_m j by auto also have "... = row B (f i) $v j" by (rule index_row[symmetric], insert B fi_m j, auto) finally show ?thesis .. - qed - show ?thesis by (rule arg_cong[of _ _ det], rule eq_matI, insert row_eq_colT, auto) - qed + qed + show ?thesis by (rule arg_cong[of _ _ det], rule eq_matI, insert row_eq_colT, auto) + qed ultimately show "(\i = 0..T $$ (f i, i)) * det (mat\<^sub>r n n (\i. col B\<^sup>T (f i))) = - (\i = 0..r n n (\i. row B (f i)))" by simp + (\i = 0..r n n (\i. row B (f i)))" by simp qed - finally show ?thesis + finally show ?thesis by (metis (no_types, lifting) A B det_transpose transpose_mult mult_carrier_mat) qed (*We need a more general version of this lemma*) lemma assumes F: "F= {f. f \ {0.. {0.. (\i. i \ {0.. f i = i)}" and p: " \ permutes {0..f\F. (\i = 0.. i))) = (\f\F. (\i = 0.. \ = g \ \" + fix f g assume fop: "f \ \ = g \ \" have "f x = g x" for x proof (cases "x \ {0.. F" show "xa \ \ \ F" - unfolding o_def F - using F PiE p xa + fix xa assume xa: "xa \ F" show "xa \ \ \ F" + unfolding o_def F + using F PiE p xa by (auto, smt F atLeastLessThan_iff mem_Collect_eq p permutes_def xa) - show "\x\F. xa = x \ \" + show "\x\F. xa = x \ \" proof (rule bexI[of _ "xa \ Hilbert_Choice.inv \"]) show "xa = xa \ Hilbert_Choice.inv \ \ \" - using p by auto - show "xa \ Hilbert_Choice.inv \ \ F" - unfolding o_def F - using F PiE p xa + using p by auto + show "xa \ Hilbert_Choice.inv \ \ F" + unfolding o_def F + using F PiE p xa by (auto, smt atLeastLessThan_iff permutes_def permutes_less(3)) qed qed have prod_rw: "(\i = 0..i = 0.. i), \ i))" if "f\F" for f using prod.permute[OF p] by auto let ?g = "\f. (\i = 0.. i))" - have "(\f\F. (\i = 0..f\F. (\i = 0.. i), \ i)))" + have "(\f\F. (\i = 0..f\F. (\i = 0.. i), \ i)))" using prod_rw by auto also have "... = (\f\(?h`F). \i = 0.. i))" using sum.reindex[OF inj_on_F, of ?g] unfolding hF by auto also have "... = (\f\F. \i = 0.. i))" unfolding hF by auto - finally show ?thesis .. + finally show ?thesis .. qed lemma detAB_Znm_aux: assumes F: "F= {f. f \ {0.. {0.. (\i. i \ {0.. f i = i)}" - shows"(\\ | \ permutes {0..f\F. prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))) - = (\\ | \ permutes {0..f\F. (\i = 0.. i)) + shows"(\\ | \ permutes {0..f\F. prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))) + = (\\ | \ permutes {0..f\F. (\i = 0.. i)) * (signof \ * (\i = 0..\ | \ permutes {0..f\F. prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))) = + have "(\\ | \ permutes {0..f\F. prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))) = (\\ | \ permutes {0..f\F. signof \ * (\i = 0.. i, f i)))" by (smt mult.left_commute prod.cong prod.distrib sum.cong) - also have "... = (\\ | \ permutes {0..f\F. signof (Hilbert_Choice.inv \) - * (\i = 0.. i, f i)))" + also have "... = (\\ | \ permutes {0..f\F. signof (Hilbert_Choice.inv \) + * (\i = 0.. i, f i)))" by (rule sum_permutations_inverse) - also have "... = (\\ | \ permutes {0..f\F. signof (Hilbert_Choice.inv \) + also have "... = (\\ | \ permutes {0..f\F. signof (Hilbert_Choice.inv \) * (\i = 0.. i), (\ i)) * A $$ (Hilbert_Choice.inv \ (\ i), f (\ i))))" proof (rule sum.cong) fix x assume x: "x \ {\. \ permutes {0..i = 0..i = 0..i = 0.. F" for f using prod.permute[OF p] by auto then show "(\f\F. signof ?inv_x * (\i = 0..f\F. signof ?inv_x * (\i = 0..\ | \ permutes {0..f\F. signof \ - * (\i = 0.. i), (\ i)) * A $$ (i, f (\ i))))" - by (rule sum.cong, auto, rule sum.cong, auto) + also have "... = (\\ | \ permutes {0..f\F. signof \ + * (\i = 0.. i), (\ i)) * A $$ (i, f (\ i))))" + by (rule sum.cong, auto, rule sum.cong, auto) (metis (no_types, lifting) finite_atLeastLessThan signof_inv) - also have "... = (\\ | \ permutes {0..f\F. signof \ + also have "... = (\\ | \ permutes {0..f\F. signof \ * (\i = 0.. i)) * A $$ (i, f i)))" proof (rule sum.cong) fix \ assume p: "\ \ {\. \ permutes {0.. permutes {0.. ?inv_pi = g \ ?inv_pi" + fix f g assume fop: "f \ ?inv_pi = g \ ?inv_pi" have "f x = g x" for x proof (cases "x \ {0.. F" show "xa \ ?inv_pi \ F" - unfolding o_def F + fix xa assume xa: "xa \ F" show "xa \ ?inv_pi \ F" + unfolding o_def F using F PiE p xa by (auto, smt atLeastLessThan_iff permutes_def permutes_less(3)) - show "\x\F. xa = x \ ?inv_pi" + show "\x\F. xa = x \ ?inv_pi" proof (rule bexI[of _ "xa \ \"]) show "xa = xa \ \ \ Hilbert_Choice.inv \ " - using p by auto - show "xa \ \ \ F" - unfolding o_def F - using F PiE p xa + using p by auto + show "xa \ \ \ F" + unfolding o_def F + using F PiE p xa by (auto, smt atLeastLessThan_iff permutes_def permutes_less(3)) qed qed let ?g = "\f. signof \ * (\i = 0.. i), \ i) * A $$ (i, f (\ i)))" show "(\f\F. signof \ * (\i = 0.. i), \ i) * A $$ (i, f (\ i)))) = (\f\F. signof \ * (\i = 0.. i) * A $$ (i, f i)))" using sum.reindex[OF inj_on_F, of "?g"] p unfolding hF unfolding o_def by auto qed (simp) - also have "... = (\\ | \ permutes {0..f\F. (\i = 0.. i)) + also have "... = (\\ | \ permutes {0..f\F. (\i = 0.. i)) * (signof \ * (\i = 0.. carrier_mat n m" and B: "B \ carrier_mat m n" - shows "det (A*B) = (\(f, \)\Z n m. signof \ * (\i = 0.. i)))" + shows "det (A*B) = (\(f, \)\Z n m. signof \ * (\i = 0.. i)))" proof - let ?V="{0.. {0.. {0.. (\i. i \ {0.. f i = i)}" by auto - have det_rw: "det (mat\<^sub>r n n (\i. B $$ (f i, i) \\<^sub>v col A (f i))) = - (prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i)))" + have det_rw: "det (mat\<^sub>r n n (\i. B $$ (f i, i) \\<^sub>v col A (f i))) = + (prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i)))" if f: "(\i\{0.. {0.. (\i. i \ {0.. f i = i)" for f by (rule det_rows_mul, insert A col_dim, auto) - have det_rw2: "det (mat\<^sub>r n n (\i. col A (f i))) + have det_rw2: "det (mat\<^sub>r n n (\i. col A (f i))) = (\\ | \ permutes {0.. * (\i = 0.. i, f i)))" if f: "f \ ?F" for f proof (unfold Determinant.det_def, auto, rule sum.cong, auto) fix x assume x: "x permutes {0..i = 0..i = 0..i = 0..i = 0.. {0..i = 0..i = 0..i = 0..r n n (\i. finsum_vec TYPE('a::comm_ring_1) n + have fin_n: "finite {0..r n n (\i. finsum_vec TYPE('a::comm_ring_1) n (\k. B $$ (k, i) \\<^sub>v Matrix.col A k) {0..f\?F. prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i))))" + also have "... = (\f\?F. prod (\i. B $$ (f i, i)) {0..r n n (\i. col A (f i))))" using det_rw by auto - also have "... = (\f\?F. prod (\i. B $$ (f i, i)) {0..\ | \ permutes {0.. * (\i = 0.. i, f (i)))))" + also have "... = (\f\?F. prod (\i. B $$ (f i, i)) {0..\ | \ permutes {0.. * (\i = 0.. i, f (i)))))" by (rule sum.cong, auto simp add: det_rw2) - also have "... = - (\f\?F. \\ | \ permutes {0..i. B $$ (f i, i)) {0.. * (\i = 0.. i, f (i)))))" + also have "... = + (\f\?F. \\ | \ permutes {0..i. B $$ (f i, i)) {0.. * (\i = 0.. i, f (i)))))" by (simp add: mult_hom.hom_sum) - also have "... = (\\ | \ permutes {0..f\?F.prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))" - by (rule VS_Connect.class_semiring.finsum_finsum_swap, + also have "... = (\\ | \ permutes {0..f\?F.prod (\i. B $$ (f i, i)) {0.. * (\i = 0.. i, f i))))" + by (rule VS_Connect.class_semiring.finsum_finsum_swap, insert finite_permutations finite_bounded_functions[OF fin_m fin_n], auto) thm detAB_Znm_aux - also have "... = (\\ | \ permutes {0..f\?F. (\i = 0.. i)) + also have "... = (\\ | \ permutes {0..f\?F. (\i = 0.. i)) * (signof \ * (\i = 0..f\?F.\\ | \ permutes {0..i = 0.. i)) - * (signof \ * (\i = 0..f\?F.\\ | \ permutes {0..i = 0.. i)) + * (signof \ * (\i = 0..f\?F.\\ | \ permutes {0.. + also have "... = (\f\?F.\\ | \ permutes {0.. * (\i = 0.. i)))" unfolding prod.distrib by (rule sum.cong, auto, rule sum.cong, auto) - also have "... = sum (\(f,\). (signof \) + also have "... = sum (\(f,\). (signof \) * (prod (\i. A$$(i,f i) * B $$ (f i, \ i)) {0.. carrier_mat n m" and B: "B \ carrier_mat m n" begin -private definition "Z_inj = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) +private definition "Z_inj = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. {\. \ permutes {0.. {0.. {0.. (\i. i \ {0.. f i = i) +private definition "Z_not_inj = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ \ inj_on f {0.. {\. \ permutes {0.. {0.. {0.. (\i. i \ {0.. f i = i) +private definition "Z_strict = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ strict_mono_on f {0.. {\. \ permutes {0.. {0.. {0.. (\i. i \ {0.. f i = i) +private definition "Z_not_strict = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ \ strict_mono_on f {0.. {\. \ permutes {0.. +private definition "weight f \ = (signof \) * (prod (\i. A$$(i,f i) * B $$ (f i, \ i)) {0.. {0.. {0.. (\i. i \ {0.. f i = i) +private definition "Z_good g = ({f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. (f`{0.. {\. \ permutes {0.. {0.. {0.. {0.. {0.. (\i. i \ {0.. f i = i) \ strict_mono_on f {0.. {0.. {0.. {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. {0.. {0.. {0.. {0.. (\i. i \ {0.. f i = i) \ \ inj_on f {0.. {0.. {0.. (\i. i \ {0.. f i = i)}" text\The Cauchy--Binet formula is proven in \url{https://core.ac.uk/download/pdf/82475020.pdf} - In that work, they define @{text "\ \ inv \ \ \"}. I had problems following this proof - in Isabelle, since I was demanded to show that such permutations commute, which is false. + In that work, they define @{text "\ \ inv \ \ \"}. I had problems following this proof + in Isabelle, since I was demanded to show that such permutations commute, which is false. It is a notation problem of the @{text "\"} operator, the author means @{text "\ \ \ \ inv \"} using the Isabelle notation (i.e., @{text "\ x = \ ((inv \) x)"}). \ lemma step_weight: fixes \ \ defines "\ \ \ \ Hilbert_Choice.inv \" assumes f_inj: "f \ F_inj" and gF: "g \ F" and pi: "\ permutes {0.. permutes {0..x \ {0.. x)" -shows "weight f \ = (signof \) * (\i = 0.. i))) + and phi: "\ permutes {0..x \ {0.. x)" +shows "weight f \ = (signof \) * (\i = 0.. i))) * (signof \) * (\i = 0.. i))" proof - let ?A = "(\i = 0.. i))) " let ?B = "(\i = 0.. i))" - have sigma: "\ permutes {0.._def - by (rule permutes_compose[OF permutes_inv[OF phi] pi]) + have sigma: "\ permutes {0.._def + by (rule permutes_compose[OF permutes_inv[OF phi] pi]) have A_rw: "?A = (\i = 0..i = 0.. i), \ (\ i)))" - by (rule prod.permute[unfolded o_def, OF phi]) - also have "... = (\i = 0.. i))" + by (rule prod.permute[unfolded o_def, OF phi]) + also have "... = (\i = 0.. i))" using fg_phi unfolding \_def unfolding o_def unfolding permutes_inverses(2)[OF phi] by auto finally have B_rw: "?B = (\i = 0.. i))" . have "(signof \) * ?A * (signof \) * ?B = (signof \) * (signof \) * ?A * ?B" by auto also have "... = signof (\ \ \) * ?A * ?B" unfolding signof_compose[OF phi sigma] by simp also have "... = signof \ * ?A * ?B" - by (metis (no_types, lifting) \_def mult.commute o_inv_o_cancel permutes_inj + by (metis (no_types, lifting) \_def mult.commute o_inv_o_cancel permutes_inj phi sigma signof_compose) also have "... = signof \ * (\i = 0..i = 0.. i))" using A_rw B_rw by auto also have "... = signof \ * (\i = 0.. i))" by auto also have "... = weight f \" unfolding weight_def by simp finally show ?thesis .. qed lemma Z_good_fun_alt_sum: - fixes g - defines "Z_good_fun \ {f. f \ {0.. {0.. (\i. i \ {0.. f i = i) + fixes g + defines "Z_good_fun \ {f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. (f`{0.. F_inj" shows "(\f\Z_good_fun. P f)= (\\\{\. \ permutes {0.. \))" proof - let ?f = "\\. g \ \" let ?P = "{\. \ permutes {0.. i < n" + fix xa i assume "xa permutes {0.. i < n" hence "xa i = i" unfolding permutes_def by auto thus "g (xa i) = i" using g i_ge_n unfolding F_inj_def by auto next fix xa assume "xa permutes {0.. xa) {0.. xb assume "\ permutes {0.. (\x. g (\ x)) ` {0.. {0.. {0..i. \ i < n \ x i = i" - and inj_on_x: "inj_on x {0.. = "\i. if i x i = g j) else i" show "x \ (\) g ` {\. \ permutes {0..], rule conjI) have "?\ i = i" if i: "i \ {0..!j. ?\ j = i" for i proof (cases "i x a = g j) = i" proof (rule theI2) show "i < n \ x a = g i" using xa_gi True by auto - fix xa assume "xa < n \ x a = g xa" thus "xa = i" - by (metis (mono_tags, lifting) F_inj_def True atLeast0LessThan + fix xa assume "xa < n \ x a = g xa" thus "xa = i" + by (metis (mono_tags, lifting) F_inj_def True atLeast0LessThan g inj_onD lessThan_iff mem_Collect_eq xa_gi) thus "xa = i" . qed thus ta: "?\ a = i" using a by auto - fix j assume tj: "?\ j = i" + fix j assume tj: "?\ j = i" show "j = a" proof (cases "j x j = g ja) = i" using tj True by auto - have "?P (THE ja. ?P ja)" + have the_ji: "(THE ja. ja < n \ x j = g ja) = i" using tj True by auto + have "?P (THE ja. ?P ja)" proof (rule theI) show "b < n \ x j = g b" using xj_gb b by auto - fix xa assume "xa < n \ x j = g xa" thus "xa = b" - by (metis (mono_tags, lifting) F_inj_def b atLeast0LessThan + fix xa assume "xa < n \ x j = g xa" thus "xa = b" + by (metis (mono_tags, lifting) F_inj_def b atLeast0LessThan g inj_onD lessThan_iff mem_Collect_eq xj_gb) qed hence "x j = g i" unfolding the_ji by auto hence "x j = x a" using xa_gi by auto then show ?thesis using inj_on_x a True unfolding inj_on_def by auto next case False then show ?thesis using tj True by auto - qed + qed qed next case False note i_ge_n = False - show ?thesis + show ?thesis proof (rule ex1I[of _ i]) show "?\ i = i" using False by simp - fix j assume tj: "?\ j = i" - show "j = i" + fix j assume tj: "?\ j = i" + show "j = i" proof (cases "j x j = g ja) < n" proof (rule theI2) show "a < n \ x j = g a" using xj_ga a by auto fix xa assume a1: "xa < n \ x j = g xa" thus "xa = a" using F_inj_def a atLeast0LessThan g inj_on_eq_iff xj_ga by fastforce show "xa < n" by (simp add: a1) - qed + qed then show ?thesis using tj i_ge_n by auto next case False then show ?thesis using tj by auto qed qed qed ultimately show "?\ permutes {0.. ?\" - proof - - have "x xa = g (THE j. j < n \ x xa = g j)" if xa: "xa < n" for xa + proof - + have "x xa = g (THE j. j < n \ x xa = g j)" if xa: "xa < n" for xa proof - obtain c where c: "c < n" and xxa_gc: "x xa = g c" by (metis (mono_tags, hide_lams) atLeast0LessThan imageE imageI lessThan_iff xa xg) show ?thesis proof (rule theI2) show c1: "c < n \ x xa = g c" using c xxa_gc by auto fix xb assume c2: "xb < n \ x xa = g xb" thus "xb = c" - by (metis (mono_tags, lifting) F_inj_def c1 atLeast0LessThan + by (metis (mono_tags, lifting) F_inj_def c1 atLeast0LessThan g inj_onD lessThan_iff mem_Collect_eq) show "x xa = g xb" using c1 c2 by simp qed qed - moreover have "x xa = g xa" if xa: "\ xa < n" for xa + moreover have "x xa = g xa" if xa: "\ xa < n" for xa using g x1 x2 xa unfolding F_inj_def by simp ultimately show ?thesis unfolding o_def fun_eq_iff by auto - qed + qed qed qed - have inj: "inj_on ?f ?P" + have inj: "inj_on ?f ?P" proof (rule inj_onI) fix x y assume x: "x \ ?P" and y: "y \ ?P" and gx_gy: "g \ x = g \ y" have "x i = y i" for i proof (cases "i {0.. {0.. {0.. {0..f\Z_good_fun. P f) = (\f\?f`?P. P f)" using fP by simp - also have "... = sum (P \ (\) g) {\. \ permutes {0.. (\) g) {\. \ permutes {0..\ | \ permutes {0.. \))" by auto finally show ?thesis . qed -lemma F_injI: - assumes "f \ {0.. {0.. {0.. {0..i. i \ {0.. f i = i)" and "inj_on f {0.. F_inj" using assms unfolding F_inj_def by simp lemma F_inj_composition_permutation: assumes phi: "\ permutes {0.. F_inj" shows "g \ \ \ F_inj" proof (rule F_injI) - show "g \ \ \ {0.. {0.. \ \ {0.. {0..i. i \ {0.. (g \ \) i = i" + show "\i. i \ {0.. (g \ \) i = i" using g phi unfolding permutes_def F_inj_def by simp - show "inj_on (g \ \) {0.. \) {0.. F_strict" +lemma F_strict_imp_F_inj: + assumes f: "f \ F_strict" shows "f \ F_inj" using f strict_mono_on_imp_inj_on unfolding F_strict_def F_inj_def by auto lemma one_step: assumes g1: "g \ F_strict" shows "det (submatrix A UNIV (g`{0..(x, y) \ Z_good g. weight x y)" (is "?lhs = ?rhs") proof - - define Z_good_fun where "Z_good_fun = {f. f \ {0.. {0.. (\i. i \ {0.. f i = i) + define Z_good_fun where "Z_good_fun = {f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. (f`{0.. F_inj" by (rule F_strict_imp_F_inj[OF g1]) - have detA: "(\\\{\. \ permutes {0.. * (\i = 0.. i)))) + have detA: "(\\\{\. \ permutes {0.. * (\i = 0.. i)))) = det (submatrix A UNIV (g`{0.. j \ g ` {0.. g ` {0.. j \ g ` {0.. g ` {0.. j \ g ` {0.. carrier_mat n n" - unfolding submatrix_def card_J using A by auto + have subA_carrier: "submatrix A UNIV (g ` {0.. carrier_mat n n" + unfolding submatrix_def card_J using A by auto have "det (submatrix A UNIV (g`{0..p | p permutes {0..i = 0..\\{\. \ permutes {0.. * (\i = 0.. i))))" + also have "... = (\\\{\. \ permutes {0.. * (\i = 0.. i))))" proof (rule sum.cong) fix x assume x: "x \ {\. \ permutes {0..i = 0..i = 0..i = 0.. {0.. {0.. (g ` {0..i = 0..i = 0..i = 0..\ \ ?Perm. signof (\ \ ?inv \) * (\i = 0.. \ ?inv \) i))) - = (\\ \ ?Perm. signof (\) * (\i = 0.. i)))" + = (\\ \ ?Perm. signof (\) * (\i = 0.. i)))" if phi: "\ permutes {0.. proof - let ?h="\\. \ \ ?inv \" let ?g = "\\. signof (\) * (\i = 0.. i))" - have "?h`?Perm = ?Perm" + have "?h`?Perm = ?Perm" proof - have "\ \ ?inv \ permutes {0.. permutes {0.. using permutes_compose permutes_inv phi that by blast moreover have "x \ (\\. \ \ ?inv \) ` ?Perm" if "x permutes {0.. \ permutes {0.. \ \ ?inv \" using phi by auto ultimately show ?thesis unfolding image_def by auto qed ultimately show ?thesis by auto qed hence "(\\ \ ?Perm. ?g \) = (\\ \ ?h`?Perm. ?g \)" by simp - also have "... = sum (?g \ ?h) ?Perm" + also have "... = sum (?g \ ?h) ?Perm" proof (rule sum.reindex) show "inj_on (\\. \ \ ?inv \) {\. \ permutes {0..\ \ ?Perm. signof (\ \ ?inv \) * (\i = 0.. \ ?inv \) i)))" unfolding o_def by auto finally show ?thesis by simp qed - have detB: "det (submatrix B (g`{0..\ \ ?Perm. signof \ * (\i = 0.. i)))" proof - have "{i. i < dim_row B \ i \ g ` {0.. g ` {0.. j \ g ` {0.. carrier_mat n n" unfolding submatrix_def using card_I B by auto - have "det (submatrix B (g`{0..p \ ?Perm. signof p - * (\i=0..p \ ?Perm. signof p + * (\i=0..\ \ ?Perm. signof \ * (\i = 0.. i)))" proof (rule sum.cong, rule refl) fix x assume x: "x \ {\. \ permutes {0..i=0..i=0.. {0.. (g ` {0..i = 0..i = 0..i = 0..f\Z_good_fun. \\\?Perm. weight f \)" + have "?rhs = (\f\Z_good_fun. \\\?Perm. weight f \)" unfolding Z_good_def sum.cartesian_product Z_good_fun_def by blast - also have "... = (\\\{\. \ permutes {0.. \))" unfolding Z_good_fun_def - by (rule Z_good_fun_alt_sum[OF g]) - also have "... = (\\\{\. \ permutes {0..\\{\. \ permutes {0.. * (\i = 0.. i))) * signof (\ \ ?inv \) + also have "... = (\\\{\. \ permutes {0.. \))" unfolding Z_good_fun_def + by (rule Z_good_fun_alt_sum[OF g]) + also have "... = (\\\{\. \ permutes {0..\\{\. \ permutes {0.. * (\i = 0.. i))) * signof (\ \ ?inv \) * (\i = 0.. \ ?inv \) i)))" proof (rule sum.cong, simp, rule sum.cong, simp) fix \ \ assume phi: "\ \ ?Perm" and pi: "\ \ ?Perm" - show "weight (g \ \) \ = signof \ * (\i = 0.. i))) * - signof (\ \ ?inv \) * (\i = 0.. \ ?inv \) i))" + show "weight (g \ \) \ = signof \ * (\i = 0.. i))) * + signof (\ \ ?inv \) * (\i = 0.. \ ?inv \) i))" proof (rule step_weight) show "g \ \ \ F_inj" by (rule F_inj_composition_permutation[OF _ g], insert phi, auto) - show "g \ F" using g unfolding F_def F_inj_def by simp + show "g \ F" using g unfolding F_def F_inj_def by simp qed (insert phi pi, auto) qed also have "... = (\\\{\. \ permutes {0.. * (\i = 0.. i))) * (\\ | \ permutes {0.. \ ?inv \) * (\i = 0.. \ ?inv \) i))))" by (metis (mono_tags, lifting) Groups.mult_ac(1) semiring_0_class.sum_distrib_left sum.cong) - also have "... = (\\ \ ?Perm. signof \ * (\i = 0.. i))) * + also have "... = (\\ \ ?Perm. signof \ * (\i = 0.. i))) * (\\ \ ?Perm. signof \ * (\i = 0.. i))))" using detB_rw by auto - also have "... = (\\ \ ?Perm. signof \ * (\i = 0.. i)))) * + also have "... = (\\ \ ?Perm. signof \ * (\i = 0.. i)))) * (\\ \ ?Perm. signof \ * (\i = 0.. i)))" by (simp add: semiring_0_class.sum_distrib_right) also have "... = ?lhs" unfolding detA detB .. finally show ?thesis .. qed lemma gather_by_strictness: -"sum (\g. sum (\(f,\). weight f \) (Z_good g)) F_strict +"sum (\g. sum (\(f,\). weight f \) (Z_good g)) F_strict = sum (\g. det (submatrix A UNIV (g`{0.. F_strict" - show "(\(x, y)\Z_good f. weight x y) + show "(\(x, y)\Z_good f. weight x y) = det (submatrix A UNIV (f ` {0..i\{0.. {0.. (\i. i \ {0.. f i = i)} = ?B" by auto have "?A\?B" by auto moreover have "finite ?B" using B finite_bounded_functions[OF finM finN] by auto ultimately show "finite ?A" using rev_finite_subset by blast show "finite {\. \ permutes {0..i\{0.. {0.. (\i. i \ {0.. f i = i)} = ?B" by auto have "?A\?B" by auto moreover have "finite ?B" using B finite_bounded_functions[OF finM finN] by auto ultimately show "finite ?A" using rev_finite_subset by blast show "finite {\. \ permutes {0..i\{0.. {0.. (\i. i \ {0.. f i = i)} = ?B" by auto have "?A\?B" by auto moreover have "finite ?B" using B finite_bounded_functions[OF finM finN] by auto ultimately show "finite ?A" using rev_finite_subset by blast show "finite {\. \ permutes {0..i\{0.. {0.. (\i. i \ {0.. f i = i)} = ?B" by auto have "?A\?B" by auto moreover have "finite ?B" using B finite_bounded_functions[OF finM finN] by auto ultimately show "finite F_inj" unfolding F_inj_def using rev_finite_subset by blast qed lemma finite_F_strict[simp]: "finite F_strict" proof - have finN: "finite {0..i\{0.. {0.. (\i. i \ {0.. f i = i)} = ?B" by auto have "?A\?B" by auto moreover have "finite ?B" using B finite_bounded_functions[OF finM finN] by auto ultimately show "finite F_strict" unfolding F_strict_def using rev_finite_subset by blast qed lemma nth_strict_mono: fixes f::"nat \ nat" assumes strictf: "strict_mono f" and i: "i ?I. a < f i} = i" using i proof (induct i) case 0 then show ?case by (auto simp add: strict_mono_less strictf) next case (Suc i) have i: "i < n" using Suc.prems by auto let ?J'="{a \ f ` {0.. f i" and 2: "f xa < f (Suc i)" + fix xa assume 1: "f xa \ f i" and 2: "f xa < f (Suc i)" show "f xa < f i" using 1 2 not_less_less_Suc_eq strict_mono_less strictf by fastforce next fix xa assume "f xa < f i" thus "f xa < f (Suc i)" using less_SucI strict_mono_less strictf by blast next show "f i \ f ` {0..card (f ` {0.. i) also have "... = pick ?I (card {a \ ?I. a < f i})" unfolding card_eq by simp also have "... = f i" by (rule pick_card_in_set, simp add: i) finally show ?thesis .. qed lemma nth_strict_mono_on: fixes f::"nat \ nat" assumes strictf: "strict_mono_on f {0.. ?I. a < f i} = i" using i proof (induct i) case 0 then show ?case - by (auto, metis (no_types, lifting) atLeast0LessThan lessThan_iff less_Suc_eq + by (auto, metis (no_types, lifting) atLeast0LessThan lessThan_iff less_Suc_eq not_less0 not_less_eq strict_mono_on_def strictf) next case (Suc i) have i: "i < n" using Suc.prems by auto let ?J'="{a \ f ` {0.. f i" and 2: "f xa < f (Suc i)" and 3: "xa < n" + fix xa assume 1: "f xa \ f i" and 2: "f xa < f (Suc i)" and 3: "xa < n" show "f xa < f i" - by (metis (full_types) 1 2 3 antisym_conv3 atLeast0LessThan i lessThan_iff - less_SucE order.asym strict_mono_onD strictf) + by (metis (full_types) 1 2 3 antisym_conv3 atLeast0LessThan i lessThan_iff + less_SucE order.asym strict_mono_onD strictf) next fix xa assume "f xa < f i" and "xa < n" thus "f xa < f (Suc i)" using less_SucI strictf - by (metis (no_types, lifting) Suc.prems atLeast0LessThan + by (metis (no_types, lifting) Suc.prems atLeast0LessThan lessI lessThan_iff less_trans strict_mono_onD) next show "f i \ f ` {0..card (f ` {0.. i) also have "... = pick ?I (card {a \ ?I. a < f i})" unfolding card_eq by simp also have "... = f i" by (rule pick_card_in_set, simp add: i) finally show ?thesis .. qed -lemma strict_fun_eq: +lemma strict_fun_eq: assumes f: "f \ F_strict" and g: "g \ F_strict" and fg: "f`{0.. F_inj" shows "strict_from_inj n f \ F" proof - - { + { fix x assume x: "x < n" have inj_on: "inj_on f {0.. a \ f ` {0.. a \ f ` {0.. F_strict" - if xa: "xa \ F_inj" for xa +lemma strict_from_inj_F_strict: "strict_from_inj n xa \ F_strict" + if xa: "xa \ F_inj" for xa proof - have "strict_mono_on (strict_from_inj n xa) {0.. F_inj" shows "strict_from_inj n f ` {0.. a \ f ` {0.. a \ f ` {0.. f ` {0..card (f ` {0.. xa) finally show "strict_from_inj n f xa \ f ` {0.. strict_from_inj n f ` {0.. F_strict" shows "Z_good g = {x \ F_inj. strict_from_inj n x = g} \ {\. \ permutes {0.. {0.. {0.. (\i. i \ {0.. f i = i) + define Z_good_fun where "Z_good_fun = {f. f \ {0.. {0.. (\i. i \ {0.. f i = i) \ inj_on f {0.. (f`{0.. F_inj. strict_from_inj n x = g}" proof (auto) fix f assume f: "f \ Z_good_fun" thus f_inj: "f \ F_inj" unfolding F_inj_def Z_good_fun_def by auto show "strict_from_inj n f = g" proof (rule strict_fun_eq[OF _ g]) - show "strict_from_inj n f ` {0.. F_strict" + show "strict_from_inj n f \ F_strict" using F_strict_def f_inj strict_from_inj_F_strict by blast qed next - fix f assume f_inj: "f \ F_inj" and g_strict_f: "g = strict_from_inj n f" + fix f assume f_inj: "f \ F_inj" and g_strict_f: "g = strict_from_inj n f" have "f xa \ g ` {0.. f ` {0.. Z_good_fun" + ultimately show "f \ Z_good_fun" using f_inj g_strict_f unfolding Z_good_fun_def F_inj_def by auto qed thus ?thesis unfolding Z_good_fun_def Z_good_def by simp qed lemma weight_0: "(\(f, \) \ Z_not_inj. weight f \) = 0" proof - let ?F="{f. (\i\{0.. {0.. (\i. i \ {0.. f i = i)}" let ?Perm = "{\. \ permutes {0..(f, \)\Z_not_inj. weight f \) + have "(\(f, \)\Z_not_inj. weight f \) = (\f \ F_not_inj. (\i = 0..r n n (\i. row B (f i))))" proof - have dim_row_rw: "dim_row (mat\<^sub>r n n (\i. col A (f i))) = n" for f by auto have dim_row_rw2: "dim_row (mat\<^sub>r n n (\i. Matrix.row B (f i))) = n" for f by auto - have prod_rw: "(\i = 0.. i)) = (\i = 0.. i)" - if f: "f \ F_not_inj" and pi: "\ \ ?Perm" for f \ + have prod_rw: "(\i = 0.. i)) = (\i = 0.. i)" + if f: "f \ F_not_inj" and pi: "\ \ ?Perm" for f \ proof (rule prod.cong, rule refl) - fix x assume x: "x \ {0.. {0.. x < dim_col B" using x pi B by auto ultimately show "B $$ (f x, \ x) = Matrix.row B (f x) $v \ x" by (rule index_row[symmetric]) qed - have sum_rw: "(\\ | \ permutes {0.. * (\i = 0.. i))) + have sum_rw: "(\\ | \ permutes {0.. * (\i = 0.. i))) = det (mat\<^sub>r n n (\i. row B (f i)))" if f: "f \ F_not_inj" for f unfolding Determinant.det_def using dim_row_rw2 prod_rw f by auto - have "(\(f, \)\Z_not_inj. weight f \) = (\f\F_not_inj.\\ \ ?Perm. weight f \)" + have "(\(f, \)\Z_not_inj. weight f \) = (\f\F_not_inj.\\ \ ?Perm. weight f \)" unfolding Z_not_inj_def unfolding sum.cartesian_product unfolding F_not_inj_def by simp - also have "... = (\f\F_not_inj. \\ | \ permutes {0.. + also have "... = (\f\F_not_inj. \\ | \ permutes {0.. * (\i = 0.. i)))" unfolding weight_def by simp - also have "... = (\f\F_not_inj. (\i = 0..\ | \ permutes {0.. * (\i = 0.. i))))" + also have "... = (\f\F_not_inj. (\i = 0..\ | \ permutes {0.. * (\i = 0.. i))))" by (rule sum.cong, rule refl, auto) (metis (no_types, lifting) mult.left_commute mult_hom.hom_sum sum.cong) - also have "... = (\f \ F_not_inj. (\i = 0..f \ F_not_inj. (\i = 0..r n n (\i. row B (f i))))" using sum_rw by auto finally show ?thesis by auto qed - also have "... = 0" + also have "... = 0" by (rule sum.neutral, insert det_not_inj_on[of _ n B], auto simp add: F_not_inj_def) finally show ?thesis . qed subsection \Final theorem\ lemma Cauchy_Binet1: - shows "det (A*B) = - sum (\f. det (submatrix A UNIV (f`{0..f. det (submatrix A UNIV (f`{0..(f, \) \ Z_not_inj. weight f \) = 0" by (rule weight_0) - let ?f = "strict_from_inj n" - have sum_rw: "sum g F_inj = (\y \ F_strict. sum g {x \ F_inj. ?f x = y})" for g - by (rule sum.group[symmetric], insert strict_from_inj_F_strict, auto) + let ?f = "strict_from_inj n" + have sum_rw: "sum g F_inj = (\y \ F_strict. sum g {x \ F_inj. ?f x = y})" for g + by (rule sum.group[symmetric], insert strict_from_inj_F_strict, auto) have Z_Union: "Z_inj \ Z_not_inj = Z n m" unfolding Z_def Z_not_inj_def Z_inj_def by auto have Z_Inter: "Z_inj \ Z_not_inj = {}" unfolding Z_def Z_not_inj_def Z_inj_def by auto have "det (A*B) = (\(f, \)\Z n m. weight f \)" using detAB_Znm[OF A B] unfolding weight_def by auto also have "... = (\(f, \)\Z_inj. weight f \) + (\(f, \)\Z_not_inj. weight f \)" by (metis Z_Inter Z_Union finite_Un finite_Znm sum.union_disjoint) also have "... = (\(f, \)\Z_inj. weight f \)" using sum0 by force - also have "... = (\f \ F_inj. \\\{\. \ permutes {0..)" + also have "... = (\f \ F_inj. \\\{\. \ permutes {0..)" unfolding Z_inj_def unfolding F_inj_def sum.cartesian_product .. - also have "... = (\y\F_strict. \f\{x \ F_inj. strict_from_inj n x = y}. + also have "... = (\y\F_strict. \f\{x \ F_inj. strict_from_inj n x = y}. sum (weight f) {\. \ permutes {0..y\F_strict. \(f,\)\({x \ F_inj. strict_from_inj n x = y} + also have "... = (\y\F_strict. \(f,\)\({x \ F_inj. strict_from_inj n x = y} \ {\. \ permutes {0..)" unfolding F_inj_def sum.cartesian_product .. - also have "... = sum (\g. sum (\(f,\). weight f \) (Z_good g)) F_strict" - using Z_good_alt by auto + also have "... = sum (\g. sum (\(f,\). weight f \) (Z_good g)) F_strict" + using Z_good_alt by auto also have "... = ?rhs" unfolding gather_by_strictness by simp finally show ?thesis . qed lemma Cauchy_Binet: "det (A*B) = (\I\{I. I\{0.. card I=n}. det (submatrix A UNIV I) * det (submatrix B I UNIV))" proof - let ?f="(\I. (\i. if i ?setI" and J: "J \ ?setI" and fI_fJ: "?f I = ?f J" + fix I J assume I: "I \ ?setI" and J: "J \ ?setI" and fI_fJ: "?f I = ?f J" have "x \ J" if x: "x \ I" for x - by (metis (mono_tags) fI_fJ I J distinct_card in_set_conv_nth mem_Collect_eq + by (metis (mono_tags) fI_fJ I J distinct_card in_set_conv_nth mem_Collect_eq sorted_list_of_set(1) sorted_list_of_set(3) subset_eq_atLeast0_lessThan_finite x) moreover have "x \ I" if x: "x \ J" for x - by (metis (mono_tags) fI_fJ I J distinct_card in_set_conv_nth mem_Collect_eq + by (metis (mono_tags) fI_fJ I J distinct_card in_set_conv_nth mem_Collect_eq sorted_list_of_set(1) sorted_list_of_set(3) subset_eq_atLeast0_lessThan_finite x) ultimately show "I = J" by auto qed have rw: "?f I ` {0.. ?setI" for I proof - - have "sorted_list_of_set I ! xa \ I" if "xa < n" for xa - by (metis (mono_tags, lifting) I distinct_card distinct_sorted_list_of_set mem_Collect_eq + have "sorted_list_of_set I ! xa \ I" if "xa < n" for xa + by (metis (mono_tags, lifting) I distinct_card distinct_sorted_list_of_set mem_Collect_eq nth_mem set_sorted_list_of_set subset_eq_atLeast0_lessThan_finite that) - moreover have "\xa\{0..I" for x - by (metis (full_types) x I atLeast0LessThan distinct_card in_set_conv_nth mem_Collect_eq + moreover have "\xa\{0..I" for x + by (metis (full_types) x I atLeast0LessThan distinct_card in_set_conv_nth mem_Collect_eq lessThan_iff sorted_list_of_set(1) sorted_list_of_set(3) subset_eq_atLeast0_lessThan_finite) ultimately show ?thesis unfolding image_def by auto qed have f_setI: "?f` ?setI = F_strict" proof - - have "sorted_list_of_set I ! xa < m" if I: "I \ {0.. {0..xa < card I\ atLeast0LessThan distinct_card finite_atLeastLessThan lessThan_iff - pick_in_set_le rev_finite_subset sorted_list_of_set(1) - sorted_list_of_set(3) sorted_list_of_set_eq_pick subsetCE) + by (metis I \xa < card I\ atLeast0LessThan distinct_card finite_atLeastLessThan lessThan_iff + pick_in_set_le rev_finite_subset sorted_list_of_set(1) + sorted_list_of_set(3) sorted_list_of_set_eq_pick subsetCE) moreover have "strict_mono_on (\i. if i < card I then sorted_list_of_set I ! i else i) {0.. {0..I \ {0.. atLeastLessThan_iff distinct_card finite_atLeastLessThan pick_mono_le - rev_finite_subset sorted_list_of_set(1) sorted_list_of_set(3) + by (smt \I \ {0.. atLeastLessThan_iff distinct_card finite_atLeastLessThan pick_mono_le + rev_finite_subset sorted_list_of_set(1) sorted_list_of_set(3) sorted_list_of_set_eq_pick strict_mono_on_def) - moreover have "x \ ?f ` {I. I \ {0.. card I = n}" + moreover have "x \ ?f ` {I. I \ {0.. card I = n}" if x1: "x \ {0.. {0..i. \ i < n \ x i = i" and s: "strict_mono_on x {0..i. if i < n then sorted_list_of_set (x ` {0..f. det (submatrix A UNIV (f ` {0.. ?f) {I. I \ {0.. card I = n}" + have "det (A*B) = sum ((\f. det (submatrix A UNIV (f ` {0.. ?f) {I. I \ {0.. card I = n}" unfolding Cauchy_Binet1 f_setI[symmetric] by (rule sum.reindex[OF inj_on]) also have "... = (\I\{I. I\{0.. card I=n}.det(submatrix A UNIV I)*det(submatrix B I UNIV))" by (rule sum.cong, insert rw, auto) finally show ?thesis . qed end end diff --git a/thys/Smith_Normal_Form/Cauchy_Binet_HOL_Analysis.thy b/thys/Smith_Normal_Form/Cauchy_Binet_HOL_Analysis.thy --- a/thys/Smith_Normal_Form/Cauchy_Binet_HOL_Analysis.thy +++ b/thys/Smith_Normal_Form/Cauchy_Binet_HOL_Analysis.thy @@ -1,119 +1,119 @@ (* Author: Jose Divasón - Email: jose.divason@unirioja.es + Email: jose.divason@unirioja.es *) section \The Cauchy--Binet formula in HOL Analysis\ theory Cauchy_Binet_HOL_Analysis - imports + imports Cauchy_Binet Perron_Frobenius.HMA_Connect begin subsection \Definition of submatrices in HOL Analysis\ definition submatrix_hma :: "'a^'nc^'nr\nat set\nat set\('a^'nc2^'nr2)" where "submatrix_hma A I J = (\ a b. A $h (from_nat (pick I (to_nat a))) $h (from_nat (pick J (to_nat b))))" context includes lifting_syntax begin -context +context fixes I::"nat set" and J::"nat set" assumes I: "card {i. i < CARD('nr::finite) \ i \ I} = CARD('nr2::finite)" assumes J: "card {i. i < CARD('nc::finite) \ i \ J} = CARD('nc2::finite)" begin lemma HMA_submatrix[transfer_rule]: "(HMA_M ===> HMA_M) (\A. submatrix A I J) ((\A. submatrix_hma A I J):: 'a^ 'nc ^ 'nr \ 'a ^ 'nc2 ^ 'nr2)" proof (intro rel_funI, goal_cases) case (1 A B) - note relAB[transfer_rule] = this - show ?case unfolding HMA_M_def + note relAB[transfer_rule] = this + show ?case unfolding HMA_M_def proof (rule eq_matI, auto) - show "dim_row (submatrix A I J) = CARD('nr2)" + show "dim_row (submatrix A I J) = CARD('nr2)" unfolding submatrix_def using I dim_row_transfer_rule relAB by force show "dim_col (submatrix A I J) = CARD('nc2)" unfolding submatrix_def using J dim_col_transfer_rule relAB by force let ?B="(submatrix_hma B I J)::'a ^ 'nc2 ^ 'nr2" fix i j assume i: "i < CARD('nr2)" and j: "j < CARD('nc2)" have i2: "i < card {i. i < dim_row A \ i \ I}" using I dim_row_transfer_rule i relAB by fastforce have j2: "j < card {j. j < dim_col A \ j \ J}" using J dim_col_transfer_rule j relAB by fastforce let ?i = "(from_nat (pick I i))::'nr" let ?j = "(from_nat (pick J j))::'nc" let ?i' = "Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2)" let ?j' = "Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2)" have i': "?i' = i" by (rule to_nat_from_nat_id[OF i]) have j': "?j' = j" by (rule to_nat_from_nat_id[OF j]) let ?f = "(\(i, j). B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2))) $h Bij_Nat.from_nat (pick J (Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2))))" have [transfer_rule]: "HMA_I (pick I i) ?i" by (simp add: Bij_Nat.to_nat_from_nat_id I i pick_le HMA_I_def) have [transfer_rule]: "HMA_I (pick J j) ?j" by (simp add: Bij_Nat.to_nat_from_nat_id J j pick_le HMA_I_def) have "submatrix A I J $$ (i, j) = A $$ (pick I i, pick J j)" by (rule submatrix_index[OF i2 j2]) also have "... = index_hma B ?i ?j" by (transfer, simp) also have "... = B $h Bij_Nat.from_nat (pick I (Bij_Nat.to_nat ((Bij_Nat.from_nat i)::'nr2))) $h - Bij_Nat.from_nat (pick J (Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2)))" + Bij_Nat.from_nat (pick J (Bij_Nat.to_nat ((Bij_Nat.from_nat j)::'nc2)))" unfolding i' j' index_hma_def by auto also have "... = ?f (i,j)" by auto - also have "... = Matrix.mat CARD('nr2) CARD('nc2) ?f $$ (i, j)" + also have "... = Matrix.mat CARD('nr2) CARD('nc2) ?f $$ (i, j)" by (rule index_mat[symmetric, OF i j]) - also have "... = from_hma\<^sub>m ?B $$ (i, j)" + also have "... = from_hma\<^sub>m ?B $$ (i, j)" unfolding from_hma\<^sub>m_def submatrix_hma_def by auto finally show "submatrix A I J $$ (i, j) = from_hma\<^sub>m ?B $$ (i, j)" . qed qed - + end end subsection \Transferring the proof from JNF to HOL Analysis\ lemma Cauchy_Binet_HOL_Analysis: fixes A::"'a::comm_ring_1^'m^'n" and B::"'a^'n^'m" - shows "Determinants.det (A**B) = (\I\{I. I\{0.. card I=nrows A}. - Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) * + shows "Determinants.det (A**B) = (\I\{I. I\{0.. card I=nrows A}. + Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) * Determinants.det ((submatrix_hma B I UNIV)::'a^'n^'n))" -proof - +proof - let ?A = "(from_hma\<^sub>m A)" let ?B = "(from_hma\<^sub>m B)" have relA[transfer_rule]: "HMA_M ?A A" unfolding HMA_M_def by simp - have relB[transfer_rule]: "HMA_M ?B B" unfolding HMA_M_def by simp - have "(\I\{I. I\{0.. card I = nrows A}. - Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) * - Determinants.det ((submatrix_hma B I UNIV)::'a^'n^'n)) = - (\I\{I. I\{0.. card I=nrows A}. det (submatrix ?A UNIV I) + have relB[transfer_rule]: "HMA_M ?B B" unfolding HMA_M_def by simp + have "(\I\{I. I\{0.. card I = nrows A}. + Determinants.det ((submatrix_hma A UNIV I)::'a^'n^'n) * + Determinants.det ((submatrix_hma B I UNIV)::'a^'n^'n)) = + (\I\{I. I\{0.. card I=nrows A}. det (submatrix ?A UNIV I) * det (submatrix ?B I UNIV))" proof (rule sum.cong) fix I assume I: "I \{I. I\{0.. card I=nrows A}" let ?sub_A= "((submatrix_hma A UNIV I)::'a^'n^'n)" let ?sub_B= "((submatrix_hma B I UNIV)::'a^'n^'n)" have c1: "card {i. i < CARD('n) \ i \ UNIV} = CARD('n)" using I by auto have c2: "card {i. i < CARD('m) \ i \ I} = CARD('n)" proof - have "I = {i. i < CARD('m) \ i \ I}" using I unfolding nrows_def ncols_def by auto thus ?thesis using I nrows_def by auto qed have [transfer_rule]: "HMA_M (submatrix ?A UNIV I) ?sub_A" using HMA_submatrix[OF c1 c2] relA unfolding rel_fun_def by auto have [transfer_rule]: "HMA_M (submatrix ?B I UNIV) ?sub_B" - using HMA_submatrix[OF c2 c1] relB unfolding rel_fun_def by auto - show "Determinants.det ?sub_A * Determinants.det ?sub_B + using HMA_submatrix[OF c2 c1] relB unfolding rel_fun_def by auto + show "Determinants.det ?sub_A * Determinants.det ?sub_B = det (submatrix ?A UNIV I) * det (submatrix ?B I UNIV)" by (transfer', auto) - qed (auto) - also have "... = det (?A*?B)" + qed (auto) + also have "... = det (?A*?B)" by (rule Cauchy_Binet[symmetric], unfold nrows_def ncols_def, auto) also have "... = Determinants.det (A**B)" by (transfer', auto) finally show ?thesis .. qed end \ No newline at end of file diff --git a/thys/Smith_Normal_Form/Rings2_Extended.thy b/thys/Smith_Normal_Form/Rings2_Extended.thy --- a/thys/Smith_Normal_Form/Rings2_Extended.thy +++ b/thys/Smith_Normal_Form/Rings2_Extended.thy @@ -1,809 +1,809 @@ (* Author: Jose Divasón - Email: jose.divason@unirioja.es + Email: jose.divason@unirioja.es *) section \Some theorems about rings and ideals\ theory Rings2_Extended - imports + imports Echelon_Form.Rings2 "HOL-Types_To_Sets.Types_To_Sets" begin subsection \Missing properties on ideals\ lemma ideal_generated_subset2: assumes "\b\B. b \ ideal_generated A" shows "ideal_generated B \ ideal_generated A" - by (metis (mono_tags, lifting) InterE assms ideal_generated_def + by (metis (mono_tags, lifting) InterE assms ideal_generated_def ideal_ideal_generated mem_Collect_eq subsetI) context comm_ring_1 begin -lemma ideal_explicit: "ideal_generated S +lemma ideal_explicit: "ideal_generated S = {y. \f U. finite U \ U \ S \ (\i\U. f i * i) = y}" by (simp add: ideal_generated_eq_left_ideal left_ideal_explicit) end lemma ideal_generated_minus: - assumes a: "a \ ideal_generated (S-{a})" + assumes a: "a \ ideal_generated (S-{a})" shows "ideal_generated S = ideal_generated (S-{a})" proof (cases "a \ S") case True note a_in_S = True - show ?thesis + show ?thesis proof show "ideal_generated S \ ideal_generated (S - {a})" proof (rule ideal_generated_subset2, auto) - fix b assume b: "b \ S" show "b \ ideal_generated (S - {a})" + fix b assume b: "b \ S" show "b \ ideal_generated (S - {a})" proof (cases "b = a") case True then show ?thesis using a by auto next case False then show ?thesis using b by (simp add: ideal_generated_in) - qed + qed qed - show "ideal_generated (S - {a}) \ ideal_generated S" + show "ideal_generated (S - {a}) \ ideal_generated S" by (rule ideal_generated_subset, auto) qed next case False then show ?thesis by simp qed lemma ideal_generated_dvd_eq: assumes a_dvd_b: "a dvd b" and a: "a \ S" and a_not_b: "a \ b" shows "ideal_generated S = ideal_generated (S - {b})" proof show "ideal_generated S \ ideal_generated (S - {b})" proof (rule ideal_generated_subset2, auto) - fix x assume x: "x \ S" + fix x assume x: "x \ S" show "x \ ideal_generated (S - {b})" proof (cases "x = b") case True obtain k where b_ak: "b = a * k" using a_dvd_b unfolding dvd_def by blast let ?f = "\c. k" have "(\i\{a}. i * ?f i) = x" using True b_ak by auto moreover have "{a} \ S - {b}" using a_not_b a by auto moreover have "finite {a}" by auto - ultimately show ?thesis + ultimately show ?thesis unfolding ideal_def by (metis True b_ak ideal_def ideal_generated_in ideal_ideal_generated insert_subset right_ideal_def) next case False then show ?thesis by (simp add: ideal_generated_in x) qed qed - show "ideal_generated (S - {b}) \ ideal_generated S" by (rule ideal_generated_subset, auto) + show "ideal_generated (S - {b}) \ ideal_generated S" by (rule ideal_generated_subset, auto) qed lemma ideal_generated_dvd_eq_diff_set: assumes i_in_I: "i\I" and i_in_J: "i \ J" and i_dvd_j: "\j\J. i dvd j" and f: "finite J" shows "ideal_generated I = ideal_generated (I - J)" using f i_in_J i_dvd_j i_in_I proof (induct J arbitrary: I) case empty then show ?case by auto next case (insert x J) have "ideal_generated I = ideal_generated (I-{x})" by (rule ideal_generated_dvd_eq[of i], insert insert.prems , auto) also have "... = ideal_generated ((I-{x}) - J)" by (rule insert.hyps, insert insert.prems insert.hyps, auto) also have "... = ideal_generated (I - insert x J)" using Diff_insert2[of I x J] by auto finally show ?case . qed context comm_ring_1 begin lemma ideal_generated_singleton_subset: assumes d: "d \ ideal_generated S" and fin_S: "finite S" shows "ideal_generated {d} \ ideal_generated S" -proof +proof fix x assume x: "x \ ideal_generated {d}" obtain k where x_kd: "x = k*d " using x using obtain_sum_ideal_generated[OF x] by (metis finite.emptyI finite.insertI sum_singleton) show "x \ ideal_generated S" using d ideal_eq_right_ideal ideal_ideal_generated right_ideal_def mult_commute x_kd by auto qed lemma ideal_generated_singleton_dvd: assumes i: "ideal_generated S = ideal_generated {d}" and x: "x \ S" shows "d dvd x" - by (metis i x finite.intros dvd_ideal_generated_singleton + by (metis i x finite.intros dvd_ideal_generated_singleton ideal_generated_in ideal_generated_singleton_subset) lemma ideal_generated_UNIV_insert: assumes "ideal_generated S = UNIV" shows "ideal_generated (insert a S) = UNIV" using assms using local.ideal_generated_subset by blast lemma ideal_generated_UNIV_union: assumes "ideal_generated S = UNIV" - shows "ideal_generated (A \ S) = UNIV" + shows "ideal_generated (A \ S) = UNIV" using assms local.ideal_generated_subset by (metis UNIV_I Un_subset_iff equalityI subsetI) -lemma ideal_explicit2: +lemma ideal_explicit2: assumes "finite S" shows "ideal_generated S = {y. \f. (\i\S. f i * i) = y}" by (smt Collect_cong assms ideal_explicit obtain_sum_ideal_generated mem_Collect_eq subsetI) lemma ideal_generated_unit: assumes u: "u dvd 1" shows "ideal_generated {u} = UNIV" proof - have "x \ ideal_generated {u}" for x proof - obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def - using local.mult_ac(2) by blast + using local.mult_ac(2) by blast have "x = x * inv_u * u" using inv_u by (simp add: local.mult_ac(1)) also have "... \ {k * u |k. k \ UNIV}" by auto also have "... = ideal_generated {u}" unfolding ideal_generated_singleton by simp finally show ?thesis . qed thus ?thesis by auto qed lemma ideal_generated_dvd_subset: assumes x: "\x \ S. d dvd x" and S: "finite S" shows "ideal_generated S \ ideal_generated {d}" -proof - fix x assume "x\ ideal_generated S" +proof + fix x assume "x\ ideal_generated S" from this obtain f where f: "(\i\S. f i * i) = x" using ideal_explicit2[OF S] by auto have "d dvd (\i\S. f i * i)" by (rule dvd_sum, insert x, auto) thus "x \ ideal_generated {d}" using f dvd_ideal_generated_singleton' ideal_generated_in singletonI by blast qed lemma ideal_generated_mult_unit: assumes f: "finite S" and u: "u dvd 1" shows "ideal_generated ((\x. u*x)` S) = ideal_generated S" using f proof (induct S) case empty then show ?case by auto next case (insert x S) obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def using mult_ac by blast have f: "finite (insert (u*x) ((\x. u*x)` S))" using insert.hyps by auto have f2: "finite (insert x S)" by (simp add: insert(1)) have f3: "finite S" by (simp add: insert) have f4: "finite ((*) u ` S)" by (simp add: insert) have inj_ux: "inj_on (\x. u*x) S" unfolding inj_on_def - by (auto, metis inv_u local.mult_1_left local.semiring_normalization_rules(18)) + by (auto, metis inv_u local.mult_1_left local.semiring_normalization_rules(18)) have "ideal_generated ((\x. u*x)` (insert x S)) = ideal_generated (insert (u*x) ((\x. u*x)` S))" by auto also have "... = {y. \f. (\i\insert (u*x) ((\x. u*x)` S). f i * i) = y}" using ideal_explicit2[OF f] by auto also have "... = {y. \f. (\i\(insert x S). f i * i) = y}" (is "?L = ?R") proof - have "a \ ?L" if a: "a \ ?R" for a proof - obtain f where sum_rw: "(\i\(insert x S). f i * i) = a" using a by auto define b where "b=(\i\S. f i * i)" have "b \ ideal_generated S" unfolding b_def ideal_explicit2[OF f3] by auto hence "b \ ideal_generated ((*) u ` S)" using insert.hyps(3) by auto - from this obtain g where "(\i\((*) u ` S). g i * i) = b" + from this obtain g where "(\i\((*) u ` S). g i * i) = b" unfolding ideal_explicit2[OF f4] by auto hence sum_rw2: "(\i\S. f i * i) = (\i\((*) u ` S). g i * i)" unfolding b_def by auto - let ?g = "\i. if i = u*x then f x * inv_u else g i" + let ?g = "\i. if i = u*x then f x * inv_u else g i" have sum_rw3: "sum ((\i. g i * i) \ (\x. u*x)) S = sum ((\i. ?g i * i) \ (\x. u*x)) S" - by (rule sum.cong, auto, metis inv_u local.insert(2) local.mult_1_right + by (rule sum.cong, auto, metis inv_u local.insert(2) local.mult_1_right local.mult_ac(2) local.semiring_normalization_rules(18)) - have sum_rw4: "(\i\(\x. u*x)` S. g i * i) = sum ((\i. g i * i) \ (\x. u*x)) S" + have sum_rw4: "(\i\(\x. u*x)` S. g i * i) = sum ((\i. g i * i) \ (\x. u*x)) S" by (rule sum.reindex[OF inj_ux]) have "a = f x * x + (\i\S. f i * i)" using sum_rw local.insert(1) local.insert(2) by auto also have "... = f x * x + (\i\(\x. u*x)` S. g i * i)" using sum_rw2 by auto - also have "... = ?g (u * x) * (u * x) + (\i\(\x. u*x)` S. g i * i)" - using inv_u by (smt local.mult_1_right local.mult_ac(1)) + also have "... = ?g (u * x) * (u * x) + (\i\(\x. u*x)` S. g i * i)" + using inv_u by (smt local.mult_1_right local.mult_ac(1)) also have "... = ?g (u * x) * (u * x) + sum ((\i. g i * i) \ (\x. u*x)) S" using sum_rw4 by auto also have "... = ((\i. ?g i * i) \ (\x. u*x)) x + sum ((\i. g i * i) \ (\x. u*x)) S" by auto - also have "... = ((\i. ?g i * i) \ (\x. u*x)) x + sum ((\i. ?g i * i) \ (\x. u*x)) S" + also have "... = ((\i. ?g i * i) \ (\x. u*x)) x + sum ((\i. ?g i * i) \ (\x. u*x)) S" using sum_rw3 by auto also have "... = sum ((\i. ?g i * i) \ (\x. u*x)) (insert x S)" by (rule sum.insert[symmetric], auto simp add: insert) also have "... = (\i\insert (u * x) ((\x. u*x)` S). ?g i * i)" - by (smt abel_semigroup.commute f2 image_insert inv_u mult.abel_semigroup_axioms mult_1_right + by (smt abel_semigroup.commute f2 image_insert inv_u mult.abel_semigroup_axioms mult_1_right semiring_normalization_rules(18) sum.reindex_nontrivial) also have "... = (\i\(\x. u*x)` (insert x S). ?g i * i)" by auto - finally show ?thesis by auto + finally show ?thesis by auto qed moreover have "a \ ?R" if a: "a \ ?L" for a proof - obtain f where sum_rw: "(\i\(insert (u * x) ((*) u ` S)). f i * i) = a" using a by auto have ux_notin: "u*x \ ((*) u ` S)" - by (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left - local.semiring_normalization_rules(18) subsetI) + by (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left + local.semiring_normalization_rules(18) subsetI) let ?f = "(\x. f x * x)" have "sum ?f ((*) u ` S) \ ideal_generated ((*) u ` S)" unfolding ideal_explicit2[OF f4] by auto - from this obtain g where sum_rw1: "sum (\i. g i * i) S = sum ?f (((*) u ` S))" + from this obtain g where sum_rw1: "sum (\i. g i * i) S = sum ?f (((*) u ` S))" using insert.hyps(3) unfolding ideal_explicit2[OF f3] by blast let ?g = "(\i. if i = x then (f (u*x) *u) * x else g i * i)" let ?g' = "\i. if i = x then f (u*x) * u else g i" - have sum_rw2: "sum (\i. g i * i) S = sum ?g S" by (rule sum.cong, insert inj_ux ux_notin, auto) + have sum_rw2: "sum (\i. g i * i) S = sum ?g S" by (rule sum.cong, insert inj_ux ux_notin, auto) have "a = (\i\(insert (u * x) ((*) u ` S)). f i * i)" using sum_rw by simp - also have "... = ?f (u*x) + sum ?f (((*) u ` S))" - by (rule sum.insert[OF f4], insert inj_ux) (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI + also have "... = ?f (u*x) + sum ?f (((*) u ` S))" + by (rule sum.insert[OF f4], insert inj_ux) (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left local.semiring_normalization_rules(18) subsetI) also have "... = ?f (u*x) + sum (\i. g i * i) S" unfolding sum_rw1 by auto also have "... = ?g x + sum ?g S" unfolding sum_rw2 using mult.assoc by auto also have "... = sum ?g (insert x S)" by (rule sum.insert[symmetric, OF f3 insert.hyps(2)]) also have "... = sum (\i. ?g' i * i) (insert x S)" by (rule sum.cong, auto) finally show ?thesis by fast qed ultimately show ?thesis by blast qed also have "... = ideal_generated (insert x S)" using ideal_explicit2[OF f2] by auto finally show ?case by auto qed corollary ideal_generated_mult_unit2: assumes u: "u dvd 1" shows "ideal_generated {u*a,u*b} = ideal_generated {a,b}" proof - let ?S = "{a,b}" have "ideal_generated {u*a,u*b} = ideal_generated ((\x. u*x)` {a,b})" by auto also have "... = ideal_generated {a,b}" by (rule ideal_generated_mult_unit[OF _ u], simp) finally show ?thesis . qed lemma ideal_generated_1[simp]: "ideal_generated {1} = UNIV" by (metis ideal_generated_unit dvd_ideal_generated_singleton order_refl) lemma ideal_generated_pair: "ideal_generated {a,b} = {p*a+q*b | p q. True}" proof - have i: "ideal_generated {a,b} = {y. \f. (\i\{a,b}. f i * i) = y}" using ideal_explicit2 by auto show ?thesis proof (cases "a=b") case True show ?thesis using True i by (auto, metis mult_ac(2) semiring_normalization_rules) (metis (no_types, hide_lams) add_minus_cancel mult_ac ring_distribs semiring_normalization_rules) next - case False + case False have 1: "\p q. (\i\{a, b}. f i * i) = p * a + q * b" for f by (rule exI[of _ "f a"], rule exI[of _ "f b"], rule sum_two_elements[OF False]) moreover have "\f. (\i\{a, b}. f i * i) = p * a + q * b" for p q - by (rule exI[of _ "\i. if i=a then p else q"], + by (rule exI[of _ "\i. if i=a then p else q"], unfold sum_two_elements[OF False], insert False, auto) - ultimately show ?thesis using i by auto + ultimately show ?thesis using i by auto qed qed lemma ideal_generated_pair_exists_pq1: assumes i: "ideal_generated {a,b} = (UNIV::'a set)" shows "\p q. p*a + q*b = 1" using i unfolding ideal_generated_pair by (smt iso_tuple_UNIV_I mem_Collect_eq) lemma ideal_generated_pair_UNIV: assumes sa_tb_u: "s*a+t*b = u" and u: "u dvd 1" shows "ideal_generated {a,b} = UNIV" proof - have f: "finite {a,b}" by simp obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def by (metis mult.commute) have "x \ ideal_generated {a,b}" for x proof (cases "a = b") case True then show ?thesis - by (metis UNIV_I dvd_def dvd_ideal_generated_singleton' ideal_generated_unit insert_absorb2 + by (metis UNIV_I dvd_def dvd_ideal_generated_singleton' ideal_generated_unit insert_absorb2 mult.commute sa_tb_u semiring_normalization_rules(34) subsetI subset_antisym u) next - case False note a_not_b = False + case False note a_not_b = False let ?f = "\y. if y = a then inv_u * x * s else inv_u * x * t" have "(\i\{a,b}. ?f i * i) = ?f a * a + ?f b * b" by (rule sum_two_elements[OF a_not_b]) - also have "... = x" using a_not_b sa_tb_u inv_u + also have "... = x" using a_not_b sa_tb_u inv_u by (auto, metis mult_ac(1) mult_ac(2) ring_distribs(1) semiring_normalization_rules(12)) finally show ?thesis unfolding ideal_explicit2[OF f] by auto qed thus ?thesis by auto qed lemma ideal_generated_pair_exists: assumes l: "(ideal_generated {a,b} = ideal_generated {d})" shows "(\ p q. p*a+q*b = d)" proof - have d: "d \ ideal_generated {d}" by (simp add: ideal_generated_in) hence "d \ ideal_generated {a,b}" using l by auto - from this obtain p q where "d = p*a+q*b" using ideal_generated_pair[of a b] by auto + from this obtain p q where "d = p*a+q*b" using ideal_generated_pair[of a b] by auto thus ?thesis by auto qed lemma obtain_ideal_generated_pair: assumes "c \ ideal_generated {a,b}" obtains p q where "p*a+q*b=c" proof - have "c \ {p * a + q * b |p q. True}" using assms ideal_generated_pair by auto thus ?thesis using that by auto qed lemma ideal_generated_pair_exists_UNIV: shows "(ideal_generated {a,b} = ideal_generated {1}) = (\p q. p*a+q*b = 1)" (is "?lhs = ?rhs") -proof - assume r: ?rhs +proof + assume r: ?rhs have "x \ ideal_generated {a,b}" for x proof (cases "a=b") case True - then show ?thesis + then show ?thesis by (metis UNIV_I r dvd_ideal_generated_singleton finite.intros ideal_generated_1 ideal_generated_pair_UNIV ideal_generated_singleton_subset) next case False have f: "finite {a,b}" by simp have 1: "1 \ ideal_generated {a,b}" using ideal_generated_pair_UNIV local.one_dvd r by blast hence i: "ideal_generated {a,b} = {y. \f. (\i\{a,b}. f i * i) = y}" - using ideal_explicit2[of "{a,b}"] by auto + using ideal_explicit2[of "{a,b}"] by auto from this obtain f where f: "f a * a + f b * b = 1" using sum_two_elements 1 False by auto let ?f = "\y. if y = a then x * f a else x * f b" - have "(\i\{a,b}. ?f i * i) = x" unfolding sum_two_elements[OF False] using f False + have "(\i\{a,b}. ?f i * i) = x" unfolding sum_two_elements[OF False] using f False using mult_ac(1) ring_distribs(1) semiring_normalization_rules(12) by force thus ?thesis unfolding i by auto qed thus ?lhs by auto next assume ?lhs thus ?rhs using ideal_generated_pair_exists[of a b 1] by auto qed corollary ideal_generated_UNIV_obtain_pair: assumes "ideal_generated {a,b} = ideal_generated {1}" shows " (\p q. p*a+q*b = d)" proof - obtain x y where "x*a+y*b = 1" using ideal_generated_pair_exists_UNIV assms by auto hence "d*x*a+d*y*b=d" using local.mult_ac(1) local.ring_distribs(1) local.semiring_normalization_rules(12) by force thus ?thesis by auto qed lemma sum_three_elements: shows "\x y z::'a. (\i\{a,b,c}. f i * i) = x * a + y * b + z * c" proof (cases "a \ b \ b \ c \ a \ c") case True then show ?thesis by (auto, metis add.assoc) next case False have 1: "\x y z. f c * c = x * c + y * c + z * c" by (rule exI[of _ 0],rule exI[of _ 0], rule exI[of _ "f c"], auto) have 2: "\x y z. f b * b + f c * c = x * b + y * b + z * c" by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], auto) have 3: "\x y z. f a * a + f c * c = x * a + y * c + z * c" by (rule exI[of _ "f a"],rule exI[of _ 0], rule exI[of _ "f c"], auto) have 4: "\x y z. (\i\{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \ c" - by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], insert a b, + by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], insert a b, auto simp add: insert_commute) - show ?thesis using False + show ?thesis using False by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4) qed lemma sum_three_elements': shows "\f::'a\'a. (\i\{a,b,c}. f i * i) = x * a + y * b + z * c" proof (cases "a \ b \ b \ c \ a \ c") case True let ?f = "\i. if i = a then x else if i = b then y else if i = c then z else 0" show ?thesis by (rule exI[of _ "?f"], insert True mult.assoc, auto simp add: local.add_ac) next - case False + case False have 1: "\f. f c * c = x * c + y * c + z * c" by (rule exI[of _ "\i. if i = c then x+y+z else 0"], auto simp add: local.ring_distribs) have 2: "\f. f a * a + f c * c = x * a + y * c + z * c" if bc: " b = c" and ac: "a \ c" by (rule exI[of _ "\i. if i = a then x else y+z"], insert ac bc add_ac ring_distribs, auto) have 3: "\f. f b * b + f c * c = x * b + y * b + z * c" if bc: " b \ c" and ac: "a = b" by (rule exI[of _ "\i. if i = a then x+y else z"], insert ac bc add_ac ring_distribs, auto) have 4: "\f. (\i\{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \ c" - by (rule exI[of _ "\i. if i = c then x+z else y"], insert a b add_ac ring_distribs, + by (rule exI[of _ "\i. if i = c then x+z else y"], insert a b add_ac ring_distribs, auto simp add: insert_commute) - show ?thesis using False + show ?thesis using False by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4) qed (*This is generalizable to arbitrary sets.*) lemma ideal_generated_triple_pair_rewrite: assumes i1: "ideal_generated {a, b, c} = ideal_generated {d}" and i2: "ideal_generated {a, b} = ideal_generated {d'}" shows "ideal_generated{d',c} = ideal_generated {d}" -proof +proof have d': "d' \ ideal_generated {a,b}" using i2 by (simp add: ideal_generated_in) show "ideal_generated {d', c} \ ideal_generated {d}" - proof + proof fix x assume x: "x \ ideal_generated {d', c}" obtain f1 f2 where f: "f1*d' + f2*c = x" using obtain_ideal_generated_pair[OF x] by auto obtain g1 g2 where g: "g1*a + g2*b = d'" using obtain_ideal_generated_pair[OF d'] by blast have 1: "f1*g1*a + f1*g2*b + f2*c = x" using f g local.ring_distribs(1) local.semiring_normalization_rules(18) by auto have "x \ ideal_generated {a, b, c}" proof - - obtain f where "(\i\{a,b,c}. f i * i) = f1*g1*a + f1*g2*b + f2*c" + obtain f where "(\i\{a,b,c}. f i * i) = f1*g1*a + f1*g2*b + f2*c" using sum_three_elements' 1 by blast - moreover have "ideal_generated {a,b,c} = {y. \f. (\i\{a,b,c}. f i * i) = y}" + moreover have "ideal_generated {a,b,c} = {y. \f. (\i\{a,b,c}. f i * i) = y}" using ideal_explicit2[of "{a,b,c}"] by simp ultimately show ?thesis using 1 by auto qed thus "x \ ideal_generated {d}" using i1 by auto qed show "ideal_generated {d} \ ideal_generated {d', c}" proof (rule ideal_generated_singleton_subset) obtain f1 f2 f3 where f: "f1*a + f2*b + f3*c = d" proof - have "d \ ideal_generated {a,b,c}" using i1 by (simp add: ideal_generated_in) from this obtain f where d: "(\i\{a,b,c}. f i * i) = d" using ideal_explicit2[of "{a,b,c}"] by auto - obtain x y z where "(\i\{a,b,c}. f i * i) = x * a + y * b + z * c" + obtain x y z where "(\i\{a,b,c}. f i * i) = x * a + y * b + z * c" using sum_three_elements by blast thus ?thesis using d that by auto qed - obtain k where k: "f1*a + f2*b = k*d'" + obtain k where k: "f1*a + f2*b = k*d'" proof - have "f1*a + f2*b \ ideal_generated{a,b}" using ideal_generated_pair by blast also have "... = ideal_generated {d'}" using i2 by simp also have "... = {k*d' |k. k\UNIV}" using ideal_generated_singleton by auto finally show ?thesis using that by auto qed have "k*d'+f3*c=d" using f k by auto thus "d \ ideal_generated {d', c}" using ideal_generated_pair by blast qed (simp) qed lemma ideal_generated_dvd: assumes i: "ideal_generated {a,b::'a} = ideal_generated{d} " and a: "d' dvd a" and b: "d' dvd b" shows "d' dvd d" proof - obtain p q where "p*a+q*b = d" using i ideal_generated_pair_exists by blast thus ?thesis using a b by auto qed lemma ideal_generated_dvd2: assumes i: "ideal_generated S = ideal_generated{d::'a} " and "finite S" and x: "\x\S. d' dvd x" -shows "d' dvd d" +shows "d' dvd d" by (metis assms dvd_ideal_generated_singleton ideal_generated_dvd_subset) end subsection \An equivalent characterization of B\'ezout rings\ text \The goal of this subsection is to prove that a ring is B\'ezout ring if and only if every finitely generated ideal is principal.\ definition "finitely_generated_ideal I = (ideal I \ (\S. finite S \ ideal_generated S = I))" -context +context assumes "SORT_CONSTRAINT('a::comm_ring_1)" begin -lemma sum_two_elements': +lemma sum_two_elements': fixes d::'a assumes s: "(\i\{a,b}. f i * i) = d" obtains p and q where "d = p * a + q * b" proof (cases "a=b") case True then show ?thesis - by (metis (no_types, lifting) add_diff_cancel_left' emptyE finite.emptyI insert_absorb2 + by (metis (no_types, lifting) add_diff_cancel_left' emptyE finite.emptyI insert_absorb2 left_diff_distrib' s sum.insert sum_singleton that) next case False show ?thesis using s unfolding sum_two_elements[OF False] - using that by auto + using that by auto qed text \This proof follows Theorem 6-3 in "First Course in Rings and Ideals" by Burton\ lemma all_fin_gen_ideals_are_principal_imp_bezout: assumes all: "\I::'a set. finitely_generated_ideal I \ principal_ideal I" shows "OFCLASS ('a, bezout_ring_class)" -proof (intro_classes) +proof (intro_classes) fix a b::'a obtain d where ideal_d: "ideal_generated {a,b} = ideal_generated {d}" using all unfolding finitely_generated_ideal_def by (metis finite.emptyI finite_insert ideal_ideal_generated principal_ideal_def) have a_in_d: "a \ ideal_generated {d}" + using ideal_d ideal_generated_subset_generator by blast + have b_in_d: "b \ ideal_generated {d}" + using ideal_d ideal_generated_subset_generator by blast + have d_in_ab: "d \ ideal_generated {a,b}" using ideal_d ideal_generated_subset_generator by auto - have b_in_d: "b \ ideal_generated {d}" - using ideal_d ideal_generated_subset_generator by auto - have d_in_ab: "d \ ideal_generated {a,b}" - using ideal_d ideal_generated_subset_generator by auto obtain f where "(\i\{a,b}. f i * i) = d" using obtain_sum_ideal_generated[OF d_in_ab] by auto from this obtain p q where d_eq: "d = p*a + q*b" using sum_two_elements' by blast moreover have d_dvd_a: "d dvd a" - by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset insert_commute + by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset insert_commute subset_insertI) moreover have "d dvd b" by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset subset_insertI) - moreover have "d' dvd d" if d'_dvd: "d' dvd a \ d' dvd b" for d' + moreover have "d' dvd d" if d'_dvd: "d' dvd a \ d' dvd b" for d' proof - - obtain s1 s2 where s1_dvd: "a = s1*d'" and s2_dvd: "b = s2*d'" + obtain s1 s2 where s1_dvd: "a = s1*d'" and s2_dvd: "b = s2*d'" using mult.commute d'_dvd unfolding dvd_def by auto have "d = p*a + q*b" using d_eq . also have "...= p * s1 * d' + q * s2 *d'" unfolding s1_dvd s2_dvd by auto also have "... = (p * s1 + q * s2) * d'" by (simp add: ring_class.ring_distribs(2)) finally show "d' dvd d" using mult.commute unfolding dvd_def by auto qed - ultimately show "\p q d. p * a + q * b = d \ d dvd a \ d dvd b + ultimately show "\p q d. p * a + q * b = d \ d dvd a \ d dvd b \ (\d'. d' dvd a \ d' dvd b \ d' dvd d)" by auto qed end context bezout_ring begin lemma exists_bezout_extended: assumes S: "finite S" and ne: "S \ {}" shows "\f d. (\a\S. f a * a) = d \ (\a\S. d dvd a) \ (\d'. (\a\S. d' dvd a) \ d' dvd d)" using S ne proof (induct S) case empty then show ?case by auto next case (insert x S) - show ?case + show ?case proof (cases "S={}") case True let ?f = "\x. 1" show ?thesis by (rule exI[of _ ?f], insert True, auto) next - case False note ne = False - note x_notin_S = insert.hyps(2) - obtain f d where sum_eq_d: "(\a\S. f a * a) = d" - and d_dvd_each_a: "(\a\S. d dvd a)" + case False note ne = False + note x_notin_S = insert.hyps(2) + obtain f d where sum_eq_d: "(\a\S. f a * a) = d" + and d_dvd_each_a: "(\a\S. d dvd a)" and d_is_gcd: "(\d'. (\a\S. d' dvd a) \ d' dvd d)" - using insert.hyps(3)[OF ne] by auto + using insert.hyps(3)[OF ne] by auto have "\p q d'. p * d + q * x = d' \ d' dvd d \ d' dvd x \ (\c. c dvd d \ c dvd x \ c dvd d')" using exists_bezout by auto from this obtain p q d' where pd_qx_d': "p*d + q*x = d'" and d'_dvd_d: "d' dvd d" and d'_dvd_x: "d' dvd x" - and d'_dvd: "\c. (c dvd d \ c dvd x) \ c dvd d'" by blast + and d'_dvd: "\c. (c dvd d \ c dvd x) \ c dvd d'" by blast let ?f = "\a. if a = x then q else p * f a" have "(\a\insert x S. ?f a * a) = d'" proof - have "(\a\insert x S. ?f a * a) = (\a\S. ?f a * a) + ?f x * x" by (simp add: add_commute insert.hyps(1) insert.hyps(2)) - also have "... = p * (\a\S. f a * a) + q * x" + also have "... = p * (\a\S. f a * a) + q * x" unfolding sum_distrib_left - by (auto, rule sum.cong, insert x_notin_S, + by (auto, rule sum.cong, insert x_notin_S, auto simp add: mult.semigroup_axioms semigroup.assoc) - finally show ?thesis using pd_qx_d' sum_eq_d by auto + finally show ?thesis using pd_qx_d' sum_eq_d by auto qed moreover have "(\a\insert x S. d' dvd a)" by (metis d'_dvd_d d'_dvd_x d_dvd_each_a insert_iff local.dvdE local.dvd_mult_left) moreover have " (\c. (\a\insert x S. c dvd a) \ c dvd d')" by (simp add: d'_dvd d_is_gcd) ultimately show ?thesis by auto qed qed end lemma ideal_generated_empty: "ideal_generated {} = {0}" unfolding ideal_generated_def using ideal_generated_0 - by (metis empty_subsetI ideal_generated_def ideal_generated_subset ideal_ideal_generated + by (metis empty_subsetI ideal_generated_def ideal_generated_subset ideal_ideal_generated ideal_not_empty subset_singletonD) lemma bezout_imp_all_fin_gen_ideals_are_principal: fixes I::"'a :: bezout_ring set" assumes fin: "finitely_generated_ideal I" shows "principal_ideal I" proof - obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I" using fin unfolding finitely_generated_ideal_def by auto - show ?thesis + show ?thesis proof (cases "S = {}") case True - then show ?thesis - using ideal_gen_S unfolding True + then show ?thesis + using ideal_gen_S unfolding True using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce next case False note ne = False obtain d f where sum_S_d: "(\i\S. f i * i) = d" and d_dvd_a: "(\a\S. d dvd a)" and d_is_gcd: "(\d'. (\a\S. d' dvd a) \ d' dvd d)" using exists_bezout_extended[OF fin_S ne] by auto have d_in_S: "d \ ideal_generated S" - by (metis fin_S ideal_def ideal_generated_subset_generator + by (metis fin_S ideal_def ideal_generated_subset_generator ideal_ideal_generated sum_S_d sum_left_ideal) - have "ideal_generated {d} \ ideal_generated S" - by (rule ideal_generated_singleton_subset[OF d_in_S fin_S]) + have "ideal_generated {d} \ ideal_generated S" + by (rule ideal_generated_singleton_subset[OF d_in_S fin_S]) moreover have "ideal_generated S \ ideal_generated {d}" - proof + proof fix x assume x_in_S: "x \ ideal_generated S" obtain f where sum_S_x: "(\a\S. f a * a) = x" using fin_S obtain_sum_ideal_generated x_in_S by blast have d_dvd_each_a: "\k. a = k * d" if "a \ S" for a by (metis d_dvd_a dvdE mult.commute that) let ?g = "\a. SOME k. a = k*d" have "x = (\a\S. f a * a)" using sum_S_x by simp - also have "... = (\a\S. f a * (?g a * d))" + also have "... = (\a\S. f a * (?g a * d))" proof (rule sum.cong) - fix a assume a_in_S: "a \ S" + fix a assume a_in_S: "a \ S" obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto - have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd) + have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd) thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto qed (simp) - also have "... = (\a\S. f a * ?g a * d)" by (rule sum.cong, auto) + also have "... = (\a\S. f a * ?g a * d)" by (rule sum.cong, auto) also have "... = (\a\S. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto finally show "x \ ideal_generated {d}" - by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right + by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right ideal_generated_in singletonI) qed ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto qed qed -text \Now we have the required lemmas to prove the theorem that states that +text \Now we have the required lemmas to prove the theorem that states that a ring is B\'ezout ring if and only if every finitely generated ideal is principal. They are the following ones. \begin{itemize} \item @{text "all_fin_gen_ideals_are_principal_imp_bezout"} \item @{text "bezout_imp_all_fin_gen_ideals_are_principal"} \end{itemize} -However, in order to prove the final lemma, we need the lemmas with no type restrictions. +However, in order to prove the final lemma, we need the lemmas with no type restrictions. For instance, we need a version of theorem @{text "bezout_imp_all_fin_gen_ideals_are_principal"} as -@{text "OFCLASS('a,bezout_ring) \"} the theorem with generic types +@{text "OFCLASS('a,bezout_ring) \"} the theorem with generic types (i.e., @{text "'a"} with no type restrictions) - + or as -@{text "class.bezout_ring _ _ _ _ \"} the theorem with generic +@{text "class.bezout_ring _ _ _ _ \"} the theorem with generic types (i.e., @{text "'a"} with no type restrictions) \ (*A possible workaround is to adapt the proof*) (* lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory: assumes a1: "class.bezout_ring ( * ) (1::'a::comm_ring_1) (+) 0 (-) uminus" (*Me da igual esto que OFCLASS*) shows "\I::'a set. finitely_generated_ideal I \ principal_ideal I" proof (rule allI, rule impI) fix I::"'a set" assume fin: "finitely_generated_ideal I" interpret a: bezout_ring "( * )" "(1::'a)" "(+)" 0 "(-)" uminus using a1 . interpret dvd "( * )::'a\'a\'a" . interpret b: comm_monoid_add "(+)" "(0::'a)" using a1 by intro_locales have c: " class.comm_monoid_add (+) (0::'a)" using a1 by intro_locales - have [simp]: "(dvd.dvd ( * ) d a) = (d dvd a)" for d a::'a + have [simp]: "(dvd.dvd ( * ) d a) = (d dvd a)" for d a::'a by (auto simp add: dvd.dvd_def dvd_def) - have [simp]: "comm_monoid_add.sum (+) 0 (\a. f a * a) S = sum (\a. f a * a) S" - for f and S::"'a set" - unfolding sum_def unfolding comm_monoid_add.sum_def[OF c] .. + have [simp]: "comm_monoid_add.sum (+) 0 (\a. f a * a) S = sum (\a. f a * a) S" + for f and S::"'a set" + unfolding sum_def unfolding comm_monoid_add.sum_def[OF c] .. obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I" using fin unfolding finitely_generated_ideal_def by auto show "principal_ideal I" proof (cases "S = {}") case True - then show ?thesis - using ideal_gen_S unfolding True + then show ?thesis + using ideal_gen_S unfolding True using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce next case False note ne = False obtain d f where sum_S_d: "(\i\S. f i * i) = d" and d_dvd_a: "(\a\S. d dvd a)" and d_is_gcd: "(\d'. (\a\S. d' dvd a) \ d' dvd d)" using a.exists_bezout_extended[OF fin_S ne] by auto have d_in_S: "d \ ideal_generated S" - by (metis fin_S ideal_def ideal_generated_subset_generator + by (metis fin_S ideal_def ideal_generated_subset_generator ideal_ideal_generated sum_S_d sum_left_ideal) - have "ideal_generated {d} \ ideal_generated S" - by (rule ideal_generated_singleton_subset[OF d_in_S fin_S]) + have "ideal_generated {d} \ ideal_generated S" + by (rule ideal_generated_singleton_subset[OF d_in_S fin_S]) moreover have "ideal_generated S \ ideal_generated {d}" - proof + proof fix x assume x_in_S: "x \ ideal_generated S" obtain f where sum_S_x: "(\a\S. f a * a) = x" using fin_S obtain_sum_ideal_generated x_in_S by blast have d_dvd_each_a: "\k. a = k * d" if "a \ S" for a by (metis d_dvd_a dvdE mult.commute that) let ?g = "\a. SOME k. a = k*d" have "x = (\a\S. f a * a)" using sum_S_x by simp - also have "... = (\a\S. f a * (?g a * d))" + also have "... = (\a\S. f a * (?g a * d))" proof (rule sum.cong) - fix a assume a_in_S: "a \ S" + fix a assume a_in_S: "a \ S" obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto - have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd) + have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd) thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto qed (simp) - also have "... = (\a\S. f a * ?g a * d)" by (rule sum.cong, auto) + also have "... = (\a\S. f a * ?g a * d)" by (rule sum.cong, auto) also have "... = (\a\S. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto finally show "x \ ideal_generated {d}" - by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right + by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right ideal_generated_in singletonI) qed ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto qed qed *) -text \Thanks to local type definitions, we can obtain it automatically by means +text \Thanks to local type definitions, we can obtain it automatically by means of @{text "internalize-sort"}.\ lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory: assumes a1: "class.bezout_ring (*) (1::'b::comm_ring_1) (+) 0 (-) uminus" (*It is algo possible to prove it using OFCLASS*) shows "\I::'b set. finitely_generated_ideal I \ principal_ideal I" - using bezout_imp_all_fin_gen_ideals_are_principal[internalize_sort "'a::bezout_ring"] + using bezout_imp_all_fin_gen_ideals_are_principal[internalize_sort "'a::bezout_ring"] using a1 by auto -text \The standard library does not connect @{text "OFCLASS"} and @{text "class.bezout_ring"} +text \The standard library does not connect @{text "OFCLASS"} and @{text "class.bezout_ring"} in both directions. Here we show that @{text "OFCLASS \ class.bezout_ring"}. \ lemma OFCLASS_bezout_ring_imp_class_bezout_ring: assumes "OFCLASS('a::comm_ring_1,bezout_ring_class)" shows "class.bezout_ring ((*)::'a\'a\'a) 1 (+) 0 (-) uminus" using assms - unfolding bezout_ring_class_def class.bezout_ring_def - using conjunctionD2[of "OFCLASS('a, comm_ring_1_class)" + unfolding bezout_ring_class_def class.bezout_ring_def + using conjunctionD2[of "OFCLASS('a, comm_ring_1_class)" "class.bezout_ring_axioms ((*)::'a\'a\'a) (+)"] by (auto, intro_locales) -text \The other implication can be obtained +text \The other implication can be obtained by thm @{text "Rings2.class.Rings2.bezout_ring.of_class.intro"} \ thm Rings2.class.Rings2.bezout_ring.of_class.intro (*OFCLASS is a proposition (Prop), and then the following statement is not valid.*) (* lemma - shows "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) + shows "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) = OFCLASS('a, bezout_ring_class)" *) (*Thus, we use the meta-equality and the meta universal quantifier.*) text \Final theorem (with OFCLASS)\ lemma bezout_ring_iff_fin_gen_principal_ideal: - "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) - \ OFCLASS('a, bezout_ring_class)" + "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) + \ OFCLASS('a, bezout_ring_class)" proof - show "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) + show "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) \ OFCLASS('a, bezout_ring_class)" using all_fin_gen_ideals_are_principal_imp_bezout [where ?'a='a] by auto - show "\I::'a::comm_ring_1 set. OFCLASS('a, bezout_ring_class) + show "\I::'a::comm_ring_1 set. OFCLASS('a, bezout_ring_class) \ finitely_generated_ideal I \ principal_ideal I" using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory[where ?'b='a] using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a] by auto qed text \Final theorem (with @{text "class.bezout_ring"})\ lemma bezout_ring_iff_fin_gen_principal_ideal2: - "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) - = (class.bezout_ring ((*)::'a\'a\'a) 1 (+) 0 (-) uminus)" + "(\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I) + = (class.bezout_ring ((*)::'a\'a\'a) 1 (+) 0 (-) uminus)" proof - show "\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I + show "\I::'a::comm_ring_1 set. finitely_generated_ideal I \ principal_ideal I \ class.bezout_ring (*) 1 (+) (0::'a) (-) uminus" - using all_fin_gen_ideals_are_principal_imp_bezout[where ?'a='a] + using all_fin_gen_ideals_are_principal_imp_bezout[where ?'a='a] using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a] by auto - show "class.bezout_ring (*) 1 (+) (0::'a) (-) uminus \ \I::'a set. - finitely_generated_ideal I \ principal_ideal I" + show "class.bezout_ring (*) 1 (+) (0::'a) (-) uminus \ \I::'a set. + finitely_generated_ideal I \ principal_ideal I" using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory by auto qed end diff --git a/thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy b/thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy --- a/thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy +++ b/thys/Smith_Normal_Form/SNF_Missing_Lemmas.thy @@ -1,1168 +1,1168 @@ (* Author: Jose Divasón Email: jose.divason@unirioja.es *) section \Missing results\ theory SNF_Missing_Lemmas imports Hermite.Hermite - Mod_Type_Connect + Mod_Type_Connect Jordan_Normal_Form.DL_Rank_Submatrix "List-Index.List_Index" begin -text \This theory presents some missing lemmas that are required for the Smith normal form -development. Some of them could be added to different AFP entries, such as the Jordan Normal +text \This theory presents some missing lemmas that are required for the Smith normal form +development. Some of them could be added to different AFP entries, such as the Jordan Normal Form AFP entry by Ren\'e Thiemann and Akihisa Yamada. However, not all the lemmas can be added directly, since some imports are required.\ hide_const (open) C hide_const (open) measure subsection \Miscellaneous lemmas\ lemma sum_two_rw: "(\i = 0..<2. f i) = (\i \ {0,1::nat}. f i)" by (rule sum.cong, auto) lemma sum_common_left: fixes f::"'a \ 'b::comm_ring_1" assumes "finite A" - shows "sum (\i. c * f i) A = c * sum f A" + shows "sum (\i. c * f i) A = c * sum f A" by (simp add: mult_hom.hom_sum) -lemma prod3_intro: +lemma prod3_intro: assumes "fst A = a" and "fst (snd A) = b" and "snd (snd A) = c" shows "A = (a,b,c)" using assms by auto subsection \Transfer rules for the HMA\_Connect file of the Perron-Frobenius development\ hide_const (open) HMA_M HMA_I to_hma\<^sub>m from_hma\<^sub>m -hide_fact (open) from_hma\<^sub>m_def from_hma_to_hma\<^sub>m HMA_M_def HMA_I_def dim_row_transfer_rule +hide_fact (open) from_hma\<^sub>m_def from_hma_to_hma\<^sub>m HMA_M_def HMA_I_def dim_row_transfer_rule dim_col_transfer_rule -context +context includes lifting_syntax begin -lemma HMA_invertible_matrix[transfer_rule]: - "((HMA_Connect.HMA_M :: _ \ 'a :: comm_ring_1 ^ 'n ^ 'n \ _) ===> (=)) invertible_mat invertible" +lemma HMA_invertible_matrix[transfer_rule]: + "((HMA_Connect.HMA_M :: _ \ 'a :: comm_ring_1 ^ 'n ^ 'n \ _) ===> (=)) invertible_mat invertible" proof (intro rel_funI, goal_cases) case (1 x y) note rel_xy[transfer_rule] = "1" - have eq_dim: "dim_col x = dim_row x" - using HMA_Connect.dim_col_transfer_rule HMA_Connect.dim_row_transfer_rule rel_xy + have eq_dim: "dim_col x = dim_row x" + using HMA_Connect.dim_col_transfer_rule HMA_Connect.dim_row_transfer_rule rel_xy by fastforce - moreover have "\A'. y ** A' = Finite_Cartesian_Product.mat 1 \ A' ** y = Finite_Cartesian_Product.mat 1" + moreover have "\A'. y ** A' = Finite_Cartesian_Product.mat 1 \ A' ** y = Finite_Cartesian_Product.mat 1" if xB: "x * B = 1\<^sub>m (dim_row x)" and Bx: "B * x = 1\<^sub>m (dim_row B)" for B proof - - let ?A' = "HMA_Connect.to_hma\<^sub>m B:: 'a :: comm_ring_1 ^ 'n ^ 'n" + let ?A' = "HMA_Connect.to_hma\<^sub>m B:: 'a :: comm_ring_1 ^ 'n ^ 'n" have rel_BA[transfer_rule]: "HMA_M B ?A'" by (metis (no_types, lifting) Bx HMA_M_def eq_dim carrier_mat_triv dim_col_mat(1) from_hma\<^sub>m_def from_hma_to_hma\<^sub>m index_mult_mat(3) index_one_mat(3) rel_xy xB) have [simp]: "dim_row B = CARD('n)" using dim_row_transfer_rule rel_BA by blast have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast have "y ** ?A' = Finite_Cartesian_Product.mat 1" using xB by (transfer, simp) moreover have "?A' ** y = Finite_Cartesian_Product.mat 1" using Bx by (transfer, simp) ultimately show ?thesis by blast qed moreover have "\B. x * B = 1\<^sub>m (dim_row x) \ B * x = 1\<^sub>m (dim_row B)" if yA: "y ** A' = Finite_Cartesian_Product.mat 1" and Ay: "A' ** y = Finite_Cartesian_Product.mat 1" for A' proof - let ?B = "(from_hma\<^sub>m A')" have [simp]: "dim_row x = CARD('n)" using dim_row_transfer_rule rel_xy by blast have [transfer_rule]: "HMA_M ?B A'" by (simp add: HMA_M_def) hence [simp]: "dim_row ?B = CARD('n)" using dim_row_transfer_rule by auto have "x * ?B = 1\<^sub>m (dim_row x)" using yA by (transfer', auto) moreover have "?B * x = 1\<^sub>m (dim_row ?B)" using Ay by (transfer', auto) ultimately show ?thesis by auto qed ultimately show ?case unfolding invertible_mat_def invertible_def inverts_mat_def by auto qed end subsection \Lemmas obtained from HOL Analysis using local type definitions\ thm Cartesian_Space.invertible_mult (*In HOL Analysis*) -thm invertible_iff_is_unit (*In HOL Analysis*) +thm invertible_iff_is_unit (*In HOL Analysis*) thm det_non_zero_imp_unit (*In JNF, but only for fields*) thm mat_mult_left_right_inverse (*In JNF, but only for fields*) - + lemma invertible_mat_zero: assumes A: "A \ carrier_mat 0 0" - shows "invertible_mat A" + shows "invertible_mat A" using A unfolding invertible_mat_def inverts_mat_def one_mat_def times_mat_def scalar_prod_def Matrix.row_def col_def carrier_mat_def by (auto, metis (no_types, lifting) cong_mat not_less_zero) lemma invertible_mult_JNF: fixes A::"'a::comm_ring_1 mat" assumes A: "A\carrier_mat n n" and B: "B\carrier_mat n n" - and inv_A: "invertible_mat A" and inv_B: "invertible_mat B" + and inv_A: "invertible_mat A" and inv_B: "invertible_mat B" shows "invertible_mat (A*B)" proof (cases "n = 0") case True then show ?thesis using assms by (simp add: invertible_mat_zero) next case False - then show ?thesis using - invertible_mult[where ?'a="'a::comm_ring_1", where ?'b="'n::finite", where ?'c="'n::finite", + then show ?thesis using + invertible_mult[where ?'a="'a::comm_ring_1", where ?'b="'n::finite", where ?'c="'n::finite", where ?'d="'n::finite", untransferred, cancel_card_constraint, OF assms] by auto qed lemma invertible_iff_is_unit_JNF: assumes A: "A \ carrier_mat n n" shows "invertible_mat A \ (Determinant.det A) dvd 1" proof (cases "n=0") case True then show ?thesis using det_dim_zero invertible_mat_zero A by auto next case False then show ?thesis using invertible_iff_is_unit[untransferred, cancel_card_constraint] A by auto qed subsection \Lemmas about matrices, submatrices and determinants\ (*This is a generalization of thm mat_mult_left_right_inverse*) thm mat_mult_left_right_inverse lemma mat_mult_left_right_inverse: fixes A :: "'a::comm_ring_1 mat" assumes A: "A \ carrier_mat n n" and B: "B \ carrier_mat n n" and AB: "A * B = 1\<^sub>m n" shows "B * A = 1\<^sub>m n" proof - have "Determinant.det (A * B) = Determinant.det (1\<^sub>m n)" using AB by auto - hence "Determinant.det A * Determinant.det B = 1" + hence "Determinant.det A * Determinant.det B = 1" using Determinant.det_mult[OF A B] det_one by auto hence det_A: "(Determinant.det A) dvd 1" and det_B: "(Determinant.det B) dvd 1" using dvd_triv_left dvd_triv_right by metis+ hence inv_A: "invertible_mat A" and inv_B: "invertible_mat B" using A B invertible_iff_is_unit_JNF by blast+ - obtain B' where inv_BB': "inverts_mat B B'" and inv_B'B: "inverts_mat B' B" + obtain B' where inv_BB': "inverts_mat B B'" and inv_B'B: "inverts_mat B' B" using inv_B unfolding invertible_mat_def by auto - have B'_carrier: "B' \ carrier_mat n n" - by (metis B inv_B'B inv_BB' carrier_matD(1) carrier_matD(2) carrier_mat_triv + have B'_carrier: "B' \ carrier_mat n n" + by (metis B inv_B'B inv_BB' carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_one_mat(3) inverts_mat_def) have "B * A * B = B" using A AB B by auto hence "B * A * (B * B') = B * B'" by (smt A AB B B'_carrier assoc_mult_mat carrier_matD(1) inv_BB' inverts_mat_def one_carrier_mat) thus ?thesis - by (metis A B carrier_matD(1) carrier_matD(2) index_mult_mat(3) inv_BB' + by (metis A B carrier_matD(1) carrier_matD(2) index_mult_mat(3) inv_BB' inverts_mat_def right_mult_one_mat') qed context comm_ring_1 begin lemma col_submatrix_UNIV: assumes "j < card {i. i < dim_col A \ i \ J}" shows "col (submatrix A UNIV J) j = col A (pick J j)" proof (rule eq_vecI) show dim_eq:"dim_vec (col (submatrix A UNIV J) j) = dim_vec (col A (pick J j))" by (simp add: dim_submatrix(1)) fix i assume "i < dim_vec (col A (pick J j))" show "col (submatrix A UNIV J) j $v i = col A (pick J j) $v i" - by (smt Collect_cong assms col_def dim_col dim_eq dim_submatrix(1) + by (smt Collect_cong assms col_def dim_col dim_eq dim_submatrix(1) eq_vecI index_vec pick_UNIV submatrix_index) qed lemma submatrix_split2: "submatrix A I J = submatrix (submatrix A I UNIV) UNIV J" (is "?lhs = ?rhs") proof (rule eq_matI) show dr: "dim_row ?lhs = dim_row ?rhs" by (simp add: dim_submatrix(1)) show dc: "dim_col ?lhs = dim_col ?rhs" by (simp add: dim_submatrix(2)) fix i j assume i: "i < dim_row ?rhs" - and j: "j < dim_col ?rhs" - have "?rhs $$ (i, j) = (submatrix A I UNIV) $$ (pick UNIV i, pick J j)" + and j: "j < dim_col ?rhs" + have "?rhs $$ (i, j) = (submatrix A I UNIV) $$ (pick UNIV i, pick J j)" proof (rule submatrix_index) - show "i < card {i. i < dim_row (submatrix A I UNIV) \ i \ UNIV}" + show "i < card {i. i < dim_row (submatrix A I UNIV) \ i \ UNIV}" by (metis (full_types) dim_submatrix(1) i) show "j < card {j. j < dim_col (submatrix A I UNIV) \ j \ J}" by (metis (full_types) dim_submatrix(2) j) qed also have "... = A $$ (pick I (pick UNIV i), pick UNIV (pick J j))" proof (rule submatrix_index) show "pick UNIV i < card {i. i < dim_row A \ i \ I}" by (metis (full_types) dr dim_submatrix(1) i pick_UNIV) show "pick J j < card {j. j < dim_col A \ j \ UNIV}" by (metis (full_types) dim_submatrix(2) j pick_le) qed - also have "... = ?lhs $$ (i,j)" + also have "... = ?lhs $$ (i,j)" proof (unfold pick_UNIV, rule submatrix_index[symmetric]) show "i < card {i. i < dim_row A \ i \ I}" by (metis (full_types) dim_submatrix(1) dr i) show "j < card {j. j < dim_col A \ j \ J}" by (metis (full_types) dim_submatrix(2) dc j) qed finally show "?lhs $$ (i, j) = ?rhs $$ (i, j)" .. qed lemma submatrix_mult: "submatrix (A*B) I J = submatrix A I UNIV * submatrix B UNIV J" (is "?lhs = ?rhs") proof (rule eq_matI) show "dim_row ?lhs = dim_row ?rhs" unfolding submatrix_def by auto show "dim_col ?lhs = dim_col ?rhs" unfolding submatrix_def by auto fix i j assume i: "i < dim_row ?rhs" and j: "j < dim_col ?rhs" have i1: "i < card {i. i < dim_row (A * B) \ i \ I}" by (metis (full_types) dim_submatrix(1) i index_mult_mat(2)) have j1: "j < card {j. j < dim_col (A * B) \ j \ J}" by (metis dim_submatrix(2) index_mult_mat(3) j) have pi: "pick I i < dim_row A" using i1 pick_le by auto have pj: "pick J j < dim_col B" using j1 pick_le by auto have row_rw: "Matrix.row (submatrix A I UNIV) i = Matrix.row A (pick I i)" using i1 row_submatrix_UNIV by auto have col_rw: "col (submatrix B UNIV J) j = col B (pick J j)" using j1 col_submatrix_UNIV by auto have "?lhs $$ (i,j) = (A*B) $$ (pick I i, pick J j)" by (rule submatrix_index[OF i1 j1]) also have "... = Matrix.row A (pick I i) \ col B (pick J j)" by (rule index_mult_mat(1)[OF pi pj]) - also have "... = Matrix.row (submatrix A I UNIV) i \ col (submatrix B UNIV J) j" - using row_rw col_rw by simp + also have "... = Matrix.row (submatrix A I UNIV) i \ col (submatrix B UNIV J) j" + using row_rw col_rw by simp also have "... = (?rhs) $$ (i,j)" by (rule index_mult_mat[symmetric], insert i j, auto) finally show "?lhs $$ (i, j) = ?rhs $$ (i, j)" . qed lemma det_singleton: assumes A: "A \ carrier_mat 1 1" - shows "det A = A $$ (0,0)" + shows "det A = A $$ (0,0)" using A unfolding carrier_mat_def Determinant.det_def by auto lemma submatrix_singleton_index: assumes A: "A \ carrier_mat n m" and an: "a < n" and bm: "b < m" shows "submatrix A {a} {b} $$ (0,0) = A $$ (a,b)" proof - have a: "{i. i = a \ i < dim_row A} = {a}" using an A unfolding carrier_mat_def by auto have b: "{i. i = b \ i < dim_col A} = {b}" using bm A unfolding carrier_mat_def by auto have "submatrix A {a} {b} $$ (0,0) = A $$ (pick {a} 0,pick {b} 0)" by (rule submatrix_index, insert a b, auto) moreover have "pick {a} 0 = a" by (auto, metis (full_types) LeastI) moreover have "pick {b} 0 = b" by (auto, metis (full_types) LeastI) ultimately show ?thesis by simp qed end lemma det_not_inj_on: assumes not_inj_on: "\ inj_on f {0..r n n (\i. Matrix.row B (f i))) = 0" proof - - obtain i j where i: "ij" - using not_inj_on unfolding inj_on_def by auto - show ?thesis + obtain i j where i: "ij" + using not_inj_on unfolding inj_on_def by auto + show ?thesis proof (rule det_identical_rows[OF _ ij i j]) let ?B="(mat\<^sub>r n n (\i. row B (f i)))" - show "row ?B i = row ?B j" + show "row ?B i = row ?B j" proof (rule eq_vecI, auto) - fix ia assume ia: "ia < n" + fix ia assume ia: "ia < n" have "row ?B i $ ia = ?B $$ (i, ia)" by (rule index_row(1), insert i ia, auto) also have "... = ?B $$ (j, ia)" by (simp add: fi_fj i ia j) also have "... = row ?B j $ ia" by (rule index_row(1)[symmetric], insert j ia, auto) finally show "row ?B i $ ia = row (mat\<^sub>r n n (\i. row B (f i))) j $ ia" by simp qed show "mat\<^sub>r n n (\i. Matrix.row B (f i)) \ carrier_mat n n" by auto qed qed lemma mat_row_transpose: "(mat\<^sub>r nr nc f)\<^sup>T = mat nc nr (\(i,j). vec_index (f j) i)" - by (rule eq_matI, auto) + by (rule eq_matI, auto) lemma obtain_inverse_matrix: - assumes A: "A \ carrier_mat n n" and i: "invertible_mat A" + assumes A: "A \ carrier_mat n n" and i: "invertible_mat A" obtains B where "inverts_mat A B" and "inverts_mat B A" and "B \ carrier_mat n n" proof - have "(\B. inverts_mat A B \ inverts_mat B A)" using i unfolding invertible_mat_def by auto from this obtain B where AB: "inverts_mat A B" and BA: "inverts_mat B A" by auto moreover have "B \ carrier_mat n n" using A AB BA unfolding carrier_mat_def inverts_mat_def by (auto, metis index_mult_mat(3) index_one_mat(3))+ - ultimately show ?thesis using that by blast + ultimately show ?thesis using that by blast qed lemma invertible_mat_smult_mat: fixes A :: "'a::comm_ring_1 mat" assumes inv_A: "invertible_mat A" and k: "k dvd 1" - shows "invertible_mat (k \\<^sub>m A)" + shows "invertible_mat (k \\<^sub>m A)" proof - obtain n where A: "A \ carrier_mat n n" using inv_A unfolding invertible_mat_def by auto have det_dvd_1: "Determinant.det A dvd 1" using inv_A invertible_iff_is_unit_JNF[OF A] by auto have "Determinant.det (k \\<^sub>m A) = k ^ dim_col A * Determinant.det A" by simp also have "... dvd 1" by (rule unit_prod, insert k det_dvd_1 dvd_power_same, force+) finally show ?thesis using invertible_iff_is_unit_JNF by (metis A smult_carrier_mat) qed -lemma invertible_mat_one[simp]: "invertible_mat (1\<^sub>m n)" +lemma invertible_mat_one[simp]: "invertible_mat (1\<^sub>m n)" unfolding invertible_mat_def using inverts_mat_def by fastforce lemma four_block_mat_dim0: assumes A: "A \ carrier_mat n n" and B: "B \ carrier_mat n 0" and C: "C \ carrier_mat 0 n" and D: "D \ carrier_mat 0 0" shows "four_block_mat A B C D = A" unfolding four_block_mat_def using assms by auto lemma det_four_block_mat_lower_right_id: assumes A: "A \ carrier_mat m m" and B: "B = 0\<^sub>m m (n-m)" and C: "C = 0\<^sub>m (n-m) m" and D: "D = 1\<^sub>m (n-m)" and "n>m" shows "Determinant.det (four_block_mat A B C D) = Determinant.det A" using assms proof (induct n arbitrary: A B C D) case 0 - then show ?case by auto + then show ?case by auto next - case (Suc n) + case (Suc n) let ?block = "(four_block_mat A B C D)" let ?B = "Matrix.mat m (n-m) (\(i,j). 0)" let ?C = "Matrix.mat (n-m) m (\(i,j). 0)" - let ?D = "1\<^sub>m (n-m)" + let ?D = "1\<^sub>m (n-m)" have mat_eq: "(mat_delete ?block n n) = four_block_mat A ?B ?C ?D" (is "?lhs = ?rhs") proof (rule eq_matI) - fix i j assume i: "i < dim_row (four_block_mat A ?B ?C ?D)" + fix i j assume i: "i < dim_row (four_block_mat A ?B ?C ?D)" and j: "j < dim_col (four_block_mat A ?B ?C ?D)" let ?f = " (if i < dim_row A then if j < dim_col A then A $$ (i, j) else B $$ (i, j - dim_col A) else if j < dim_col A then C $$ (i - dim_row A, j) else D $$ (i - dim_row A, j - dim_col A))" let ?g = "(if i < dim_row A then if j < dim_col A then A $$ (i, j) else ?B $$ (i, j - dim_col A) else if j < dim_col A then ?C $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))" - have "(mat_delete ?block n n) $$ (i,j) = ?block $$ (i,j)" + have "(mat_delete ?block n n) $$ (i,j) = ?block $$ (i,j)" using i j Suc.prems unfolding mat_delete_def by auto - also have "... = ?f" + also have "... = ?f" by (rule index_mat_four_block, insert Suc.prems i j, auto) - also have "... = ?g" using i j Suc.prems by auto + also have "... = ?g" using i j Suc.prems by auto also have "... = four_block_mat A ?B ?C ?D $$ (i,j)" by (rule index_mat_four_block[symmetric], insert Suc.prems i j, auto) - finally show "?lhs $$ (i,j) = ?rhs $$ (i,j)" . + finally show "?lhs $$ (i,j) = ?rhs $$ (i,j)" . qed (insert Suc.prems, auto) have nn_1: "?block $$ (n, n) = 1" using Suc.prems by auto have rw0: "(\i {..ii carrier_mat 1 n" and B: "B \ carrier_mat m n" and m0: "m \ 0" and r: "Matrix.row A 0 = Matrix.row B 0" shows "Matrix.row (A * V) 0 = Matrix.row (B * V) 0" -proof (rule eq_vecI) +proof (rule eq_vecI) show "dim_vec (Matrix.row (A * V) 0) = dim_vec (Matrix.row (B * V) 0)" using A B r by auto fix i assume i: "i < dim_vec (Matrix.row (B * V) 0)" have "Matrix.row (A * V) 0 $v i = (A * V) $$ (0,i)" by (rule index_row, insert i A, auto) also have "... = Matrix.row A 0 \ col V i" by (rule index_mult_mat, insert A i, auto) also have "... = Matrix.row B 0 \ col V i" using r by auto also have "... = (B * V) $$ (0,i)" by (rule index_mult_mat[symmetric], insert m0 B i, auto) also have "... = Matrix.row (B * V) 0 $v i" by (rule index_row[symmetric], insert i B m0, auto) finally show "Matrix.row (A * V) 0 $v i = Matrix.row (B * V) 0 $v i" . qed lemma smult_mat_mat_one_element: assumes A: "A \ carrier_mat 1 1" and B: "B \ carrier_mat 1 n" - shows "A * B = A $$ (0,0) \\<^sub>m B" + shows "A * B = A $$ (0,0) \\<^sub>m B" proof (rule eq_matI) fix i j assume i: "i < dim_row (A $$ (0, 0) \\<^sub>m B)" and j: "j < dim_col (A $$ (0, 0) \\<^sub>m B)" have i0: "i = 0" using A B i by auto - have "(A * B) $$ (i, j) = Matrix.row A i \ col B j" + have "(A * B) $$ (i, j) = Matrix.row A i \ col B j" by (rule index_mult_mat, insert i j A B, auto) - also have "... = Matrix.row A i $v 0 * col B j $v 0" unfolding scalar_prod_def using B by auto + also have "... = Matrix.row A i $v 0 * col B j $v 0" unfolding scalar_prod_def using B by auto also have "... = A$$(i,i) * B$$(i,j)" using A i i0 j by auto - also have "... = (A $$ (i, i) \\<^sub>m B) $$ (i, j)" + also have "... = (A $$ (i, i) \\<^sub>m B) $$ (i, j)" unfolding i by (rule index_smult_mat[symmetric], insert i j B, auto) - finally show "(A * B) $$ (i, j) = (A $$ (0, 0) \\<^sub>m B) $$ (i, j)" using i0 by simp + finally show "(A * B) $$ (i, j) = (A $$ (0, 0) \\<^sub>m B) $$ (i, j)" using i0 by simp qed (insert A B, auto) lemma determinant_one_element: assumes A: "A \ carrier_mat 1 1" shows "Determinant.det A = A $$ (0,0)" -proof - +proof - have "Determinant.det A = prod_list (diag_mat A)" by (rule det_upper_triangular[OF _ A], insert A, unfold upper_triangular_def, auto) also have "... = A $$ (0,0)" using A unfolding diag_mat_def by auto finally show ?thesis . qed lemma invertible_mat_transpose: assumes inv_A: "invertible_mat (A::'a::comm_ring_1 mat)" shows "invertible_mat A\<^sup>T" proof - - obtain n where A: "A \ carrier_mat n n" + obtain n where A: "A \ carrier_mat n n" using inv_A unfolding invertible_mat_def square_mat.simps by auto hence At: "A\<^sup>T \ carrier_mat n n" by simp have "Determinant.det A\<^sup>T = Determinant.det A" - by (metis Determinant.det_def Determinant.det_transpose carrier_matI + by (metis Determinant.det_def Determinant.det_transpose carrier_matI index_transpose_mat(2) index_transpose_mat(3)) also have "... dvd 1" using invertible_iff_is_unit_JNF[OF A] inv_A by simp finally show ?thesis using invertible_iff_is_unit_JNF[OF At] by auto qed lemma dvd_elements_mult_matrix_left: assumes A: "(A::'a::comm_ring_1 mat) \ carrier_mat m n" and P: "P \ carrier_mat m m" and x: "(\i j. i j x dvd A$$(i,j))" shows "(\i j. i j x dvd (P*A)$$(i,j))" proof - have "x dvd (P * A) $$ (i, j)" if i: "i < m" and j: "j < n" for i j proof - - have "(P * A) $$ (i, j) = (\ia = 0..ia = 0..ia = 0.. carrier_mat m n" and Q: "Q \ carrier_mat n n" and x: "(\i j. i j x dvd A$$(i,j))" shows "(\i j. i j x dvd (A*Q)$$(i,j))" proof - have "x dvd (A*Q) $$ (i, j)" if i: "i < m" and j: "j < n" for i j proof - - have "(A*Q) $$ (i, j) = (\ia = 0..ia = 0..ia = 0.. carrier_mat m n" and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" and x: "(\i j. i j x dvd A$$(i,j))" shows "(\i j. i j x dvd (P*A*Q)$$(i,j))" - using dvd_elements_mult_matrix_left[OF A P x] + using dvd_elements_mult_matrix_left[OF A P x] by (meson P A Q dvd_elements_mult_matrix_right mult_carrier_mat) definition append_cols :: "'a :: zero mat \ 'a mat \ 'a mat" (infixr "@\<^sub>c" 65)where "A @\<^sub>c B = four_block_mat A B (0\<^sub>m 0 (dim_col A)) (0\<^sub>m 0 (dim_col B))" lemma append_cols_carrier[simp,intro]: - "A \ carrier_mat n a \ B \ carrier_mat n b \ (A @\<^sub>c B) \ carrier_mat n (a+b)" + "A \ carrier_mat n a \ B \ carrier_mat n b \ (A @\<^sub>c B) \ carrier_mat n (a+b)" unfolding append_cols_def by auto lemma append_cols_mult_left: assumes A: "A \ carrier_mat n a" and B: "B \ carrier_mat n b" and P: "P \ carrier_mat n n" shows "P * (A @\<^sub>c B) = (P*A) @\<^sub>c (P*B)" proof - let ?P = "four_block_mat P (0\<^sub>m n 0) (0\<^sub>m 0 n) (0\<^sub>m 0 0)" have "P = ?P" by (rule eq_matI, auto) hence "P * (A @\<^sub>c B) = ?P * (A @\<^sub>c B)" by simp - also have "?P * (A @\<^sub>c B) = four_block_mat (P * A + 0\<^sub>m n 0 * 0\<^sub>m 0 (dim_col A)) + also have "?P * (A @\<^sub>c B) = four_block_mat (P * A + 0\<^sub>m n 0 * 0\<^sub>m 0 (dim_col A)) (P * B + 0\<^sub>m n 0 * 0\<^sub>m 0 (dim_col B)) (0\<^sub>m 0 n * A + 0\<^sub>m 0 0 * 0\<^sub>m 0 (dim_col A)) - (0\<^sub>m 0 n * B + 0\<^sub>m 0 0 * 0\<^sub>m 0 (dim_col B))" unfolding append_cols_def + (0\<^sub>m 0 n * B + 0\<^sub>m 0 0 * 0\<^sub>m 0 (dim_col B))" unfolding append_cols_def by (rule mult_four_block_mat, insert A B P, auto) also have "... = four_block_mat (P * A) (P * B) (0\<^sub>m 0 (dim_col (P*A))) (0\<^sub>m 0 (dim_col (P*B)))" by (rule cong_four_block_mat, insert P, auto) also have "... = (P*A) @\<^sub>c (P*B)" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_mult_right_id: assumes A: "(A::'a::semiring_1 mat) \ carrier_mat n 1" and B: "B \ carrier_mat n (m-1)" and C: "C = four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) D" and D: "D \ carrier_mat (m-1) (m-1)" shows "(A @\<^sub>c B) * C = A @\<^sub>c (B * D)" proof - let ?C = "four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) D" have "(A @\<^sub>c B) * C = (A @\<^sub>c B) * ?C" unfolding C by auto also have "... = four_block_mat A B (0\<^sub>m 0 (dim_col A)) (0\<^sub>m 0 (dim_col B)) * ?C" unfolding append_cols_def by auto also have "... = four_block_mat (A * 1\<^sub>m 1 + B * 0\<^sub>m (m - 1) 1) (A * 0\<^sub>m 1 (m - 1) + B * D) - (0\<^sub>m 0 (dim_col A) * 1\<^sub>m 1 + 0\<^sub>m 0 (dim_col B) * 0\<^sub>m (m - 1) 1) + (0\<^sub>m 0 (dim_col A) * 1\<^sub>m 1 + 0\<^sub>m 0 (dim_col B) * 0\<^sub>m (m - 1) 1) (0\<^sub>m 0 (dim_col A) * 0\<^sub>m 1 (m - 1) + 0\<^sub>m 0 (dim_col B) * D)" by (rule mult_four_block_mat, insert assms, auto) also have "... = four_block_mat A (B * D) (0\<^sub>m 0 (dim_col A)) (0\<^sub>m 0 (dim_col (B*D)))" by (rule cong_four_block_mat, insert assms, auto) also have "... = A @\<^sub>c (B * D)" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_mult_right_id2: assumes A: "(A::'a::semiring_1 mat) \ carrier_mat n a" and B: "B \ carrier_mat n b" and C: "C = four_block_mat D (0\<^sub>m a b) (0\<^sub>m b a) (1\<^sub>m b)" and D: "D \ carrier_mat a a" shows "(A @\<^sub>c B) * C = (A * D) @\<^sub>c B" proof - let ?C = "four_block_mat D (0\<^sub>m a b) (0\<^sub>m b a) (1\<^sub>m b)" have "(A @\<^sub>c B) * C = (A @\<^sub>c B) * ?C" unfolding C by auto - also have "... = four_block_mat A B (0\<^sub>m 0 a) (0\<^sub>m 0 b) * ?C" + also have "... = four_block_mat A B (0\<^sub>m 0 a) (0\<^sub>m 0 b) * ?C" unfolding append_cols_def using A B by auto - also have "... = four_block_mat (A * D + B * 0\<^sub>m b a) (A * 0\<^sub>m a b + B * 1\<^sub>m b) + also have "... = four_block_mat (A * D + B * 0\<^sub>m b a) (A * 0\<^sub>m a b + B * 1\<^sub>m b) (0\<^sub>m 0 a * D + 0\<^sub>m 0 b * 0\<^sub>m b a) (0\<^sub>m 0 a * 0\<^sub>m a b + 0\<^sub>m 0 b * 1\<^sub>m b)" by (rule mult_four_block_mat, insert A B C D, auto) also have "... = four_block_mat (A * D) B (0\<^sub>m 0 (dim_col (A*D))) (0\<^sub>m 0 (dim_col B))" by (rule cong_four_block_mat, insert assms, auto) also have "... = (A * D) @\<^sub>c B" unfolding append_cols_def by auto finally show ?thesis . qed lemma append_cols_nth: assumes A: "A \ carrier_mat n a" and B: "B \ carrier_mat n b" and i: "ic B) $$ (i, j) = (if j < dim_col A then A $$(i,j) else B$$(i,j-a))" (is "?lhs = ?rhs") proof - let ?C = "(0\<^sub>m 0 (dim_col A))" let ?D = "(0\<^sub>m 0 (dim_col B))" have i2: "i < dim_row A + dim_row ?D" using i A by auto have j2: "j < dim_col A + dim_col (0\<^sub>m 0 (dim_col B))" using j B A by auto have "(A @\<^sub>c B) $$ (i, j) = four_block_mat A B ?C ?D $$ (i, j)" unfolding append_cols_def by auto - also have "... = (if i < dim_row A then if j < dim_col A then A $$ (i, j) - else B $$ (i, j - dim_col A) else if j < dim_col A then ?C $$ (i - dim_row A, j) + also have "... = (if i < dim_row A then if j < dim_col A then A $$ (i, j) + else B $$ (i, j - dim_col A) else if j < dim_col A then ?C $$ (i - dim_row A, j) else 0\<^sub>m 0 (dim_col B) $$ (i - dim_row A, j - dim_col A))" by (rule index_mat_four_block(1)[OF i2 j2]) also have "... = ?rhs" using i A by auto finally show ?thesis . qed lemma append_cols_split: assumes d: "dim_col A > 0" - shows "A = mat_of_cols (dim_row A) [col A 0] @\<^sub>c + shows "A = mat_of_cols (dim_row A) [col A 0] @\<^sub>c mat_of_cols (dim_row A) (map (col A) [1..c ?A2") -proof (rule eq_matI) +proof (rule eq_matI) fix i j assume i: "i < dim_row (?A1 @\<^sub>c ?A2)" and j: "j < dim_col (?A1 @\<^sub>c ?A2)" have "(?A1 @\<^sub>c ?A2) $$ (i, j) = (if j < dim_col ?A1 then ?A1 $$(i,j) else ?A2$$(i,j-(dim_col ?A1)))" - by (rule append_cols_nth, insert i j, auto simp add: append_cols_def) + by (rule append_cols_nth, insert i j, auto simp add: append_cols_def) also have "... = A $$ (i,j)" proof (cases "j< dim_col ?A1") case True then show ?thesis - by (metis One_nat_def Suc_eq_plus1 add.right_neutral append_cols_def col_def i - index_mat_four_block(2) index_vec index_zero_mat(2) less_one list.size(3) list.size(4) + by (metis One_nat_def Suc_eq_plus1 add.right_neutral append_cols_def col_def i + index_mat_four_block(2) index_vec index_zero_mat(2) less_one list.size(3) list.size(4) mat_of_cols_Cons_index_0 mat_of_cols_carrier(2) mat_of_cols_carrier(3)) next case False then show ?thesis - by (metis (no_types, lifting) Suc_eq_plus1 Suc_less_eq Suc_pred add_diff_cancel_right' append_cols_def - diff_zero i index_col index_mat_four_block(2) index_mat_four_block(3) index_zero_mat(2) - index_zero_mat(3) j length_map length_upt linordered_semidom_class.add_diff_inverse list.size(3) - list.size(4) mat_of_cols_carrier(2) mat_of_cols_carrier(3) mat_of_cols_index nth_map_upt + by (metis (no_types, lifting) Suc_eq_plus1 Suc_less_eq Suc_pred add_diff_cancel_right' append_cols_def + diff_zero i index_col index_mat_four_block(2) index_mat_four_block(3) index_zero_mat(2) + index_zero_mat(3) j length_map length_upt linordered_semidom_class.add_diff_inverse list.size(3) + list.size(4) mat_of_cols_carrier(2) mat_of_cols_carrier(3) mat_of_cols_index nth_map_upt plus_1_eq_Suc upt_0) qed finally show "A $$ (i, j) = (?A1 @\<^sub>c ?A2) $$ (i, j)" .. qed (auto simp add: append_cols_def d) lemma append_rows_nth: assumes A: "A \ carrier_mat a n" and B: "B \ carrier_mat b n" and i: "ir B) $$ (i, j) = (if i < dim_row A then A $$(i,j) else B$$(i-a,j))" (is "?lhs = ?rhs") proof - let ?C = "(0\<^sub>m (dim_row A) 0)" let ?D = "(0\<^sub>m (dim_row B) 0)" have i2: "i < dim_row A + dim_row ?D" using i j A B by auto have j2: "j < dim_col A + dim_col ?D" using i j A B by auto have "(A @\<^sub>r B) $$ (i, j) = four_block_mat A ?C B ?D $$ (i, j)" unfolding append_rows_def by auto also have "... = (if i < dim_row A then if j < dim_col A then A $$ (i, j) else ?C $$ (i, j - dim_col A) - else if j < dim_col A then B $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))" + else if j < dim_col A then B $$ (i - dim_row A, j) else ?D $$ (i - dim_row A, j - dim_col A))" by (rule index_mat_four_block(1)[OF i2 j2]) also have "... = ?rhs" using i A j B by auto finally show ?thesis . qed lemma append_rows_split: assumes k: "k\dim_row A" - shows "A = (mat_of_rows (dim_col A) [Matrix.row A i. i \ [0..r + shows "A = (mat_of_rows (dim_col A) [Matrix.row A i. i \ [0..r (mat_of_rows (dim_col A) [Matrix.row A i. i \ [k..r ?A2") proof (rule eq_matI) - have "(?A1 @\<^sub>r ?A2) \ carrier_mat (k + (dim_row A-k)) (dim_col A)" + have "(?A1 @\<^sub>r ?A2) \ carrier_mat (k + (dim_row A-k)) (dim_col A)" by (rule carrier_append_rows, insert k, auto) hence A1_A2: "(?A1 @\<^sub>r ?A2) \ carrier_mat (dim_row A) (dim_col A)" using k by simp thus "dim_row A = dim_row (?A1 @\<^sub>r ?A2)" and "dim_col A = dim_col (?A1 @\<^sub>r ?A2)" by auto fix i j assume i: "i < dim_row (?A1 @\<^sub>r ?A2)" and j: "j < dim_col (?A1 @\<^sub>r ?A2)" have "(?A1 @\<^sub>r ?A2) $$ (i, j) = (if i < dim_row ?A1 then ?A1 $$(i,j) else ?A2$$(i-(dim_row ?A1),j))" - by (rule append_rows_nth, insert k i j, auto simp add: append_rows_def) + by (rule append_rows_nth, insert k i j, auto simp add: append_rows_def) also have "... = A $$ (i,j)" proof (cases "ir ?A2) $$ (i,j)" by simp qed lemma transpose_mat_append_rows: assumes A: "A \ carrier_mat a n" and B: "B \ carrier_mat b n" shows "(A @\<^sub>r B)\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T" by (smt append_cols_def append_rows_def A B carrier_matD(1) index_transpose_mat(3) transpose_four_block_mat zero_carrier_mat zero_transpose_mat) lemma transpose_mat_append_cols: assumes A: "A \ carrier_mat n a" and B: "B \ carrier_mat n b" shows "(A @\<^sub>c B)\<^sup>T = A\<^sup>T @\<^sub>r B\<^sup>T" - by (metis Matrix.transpose_transpose A B carrier_matD(1) carrier_mat_triv + by (metis Matrix.transpose_transpose A B carrier_matD(1) carrier_mat_triv index_transpose_mat(3) transpose_mat_append_rows) lemma append_rows_mult_right: - assumes A: "(A::'a::comm_semiring_1 mat) \ carrier_mat a n" and B: "B \ carrier_mat b n" + assumes A: "(A::'a::comm_semiring_1 mat) \ carrier_mat a n" and B: "B \ carrier_mat b n" and Q: "Q\ carrier_mat n n" shows "(A @\<^sub>r B) * Q = (A * Q) @\<^sub>r (B*Q)" proof - - have "transpose_mat ((A @\<^sub>r B) * Q) = Q\<^sup>T * (A @\<^sub>r B)\<^sup>T" + have "transpose_mat ((A @\<^sub>r B) * Q) = Q\<^sup>T * (A @\<^sub>r B)\<^sup>T" by (rule transpose_mult, insert A B Q, auto) also have "... = Q\<^sup>T * (A\<^sup>T @\<^sub>c B\<^sup>T)" using transpose_mat_append_rows assms by metis - also have "... = Q\<^sup>T * A\<^sup>T @\<^sub>c Q\<^sup>T * B\<^sup>T" + also have "... = Q\<^sup>T * A\<^sup>T @\<^sub>c Q\<^sup>T * B\<^sup>T" using append_cols_mult_left assms by (metis transpose_carrier_mat) also have "transpose_mat ... = (A * Q) @\<^sub>r (B*Q)" - by (smt A B Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def Q - carrier_mat_triv index_mult_mat(2) index_transpose_mat(2) transpose_four_block_mat + by (smt A B Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def Q + carrier_mat_triv index_mult_mat(2) index_transpose_mat(2) transpose_four_block_mat zero_carrier_mat zero_transpose_mat) finally show ?thesis by simp qed lemma append_rows_mult_left_id: assumes A: "(A::'a::comm_semiring_1 mat) \ carrier_mat 1 n" and B: "B \ carrier_mat (m-1) n" and C: "C = four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) D" and D: "D \ carrier_mat (m-1) (m-1)" shows "C * (A @\<^sub>r B) = A @\<^sub>r (D * B)" proof - have "transpose_mat (C * (A @\<^sub>r B)) = (A @\<^sub>r B)\<^sup>T * C\<^sup>T" - by (metis (no_types, lifting) B C D Matrix.transpose_mult append_rows_def A carrier_matD + by (metis (no_types, lifting) B C D Matrix.transpose_mult append_rows_def A carrier_matD carrier_mat_triv index_mat_four_block(2,3) index_zero_mat(2) one_carrier_mat) also have "... = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T" using transpose_mat_append_rows[OF A B] by auto also have "... = A\<^sup>T @\<^sub>c (B\<^sup>T * D\<^sup>T)" by (rule append_cols_mult_right_id, insert A B C D, auto) - also have "transpose_mat ... = A @\<^sub>r (D * B)" - by (smt B D Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def A + also have "transpose_mat ... = A @\<^sub>r (D * B)" + by (smt B D Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def A carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_transpose_mat(3) transpose_four_block_mat zero_carrier_mat zero_transpose_mat) finally show ?thesis by auto qed lemma append_rows_mult_left_id2: assumes A: "(A::'a::comm_semiring_1 mat) \ carrier_mat a n" and B: "B \ carrier_mat b n" and C: "C = four_block_mat D (0\<^sub>m a b) (0\<^sub>m b a) (1\<^sub>m b)" and D: "D \ carrier_mat a a" shows "C * (A @\<^sub>r B) = (D * A) @\<^sub>r B" proof - have "(C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T" by (rule transpose_mult, insert assms, auto) also have "... = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T" by (metis A B transpose_mat_append_rows) also have "... = (A\<^sup>T * D\<^sup>T @\<^sub>c B\<^sup>T)" by (rule append_cols_mult_right_id2, insert assms, auto) also have "...\<^sup>T = (D * A) @\<^sub>r B" by (metis A B D transpose_mult transpose_transpose mult_carrier_mat transpose_mat_append_rows) finally show ?thesis by simp qed lemma four_block_mat_preserves_column: assumes A: "(A::'a::semiring_1 mat) \ carrier_mat n m" and B: "B = four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) C" - and C: "C \ carrier_mat (m-1) (m-1)" + and C: "C \ carrier_mat (m-1) (m-1)" and i: "ic ?A2" by (rule append_cols_split[of A, unfolded n2], insert m A, auto) hence "A * B = (?A1 @\<^sub>c ?A2) * B" by simp also have "... = ?A1 @\<^sub>c (?A2 * C)" by (rule append_cols_mult_right_id[OF _ _ B C], insert A, auto) also have "... $$ (i,0) = ?A1 $$ (i,0)" using append_cols_nth by (simp add: append_cols_def i) also have "... = A $$ (i,0)" by (metis A i carrier_matD(1) col_def index_vec mat_of_cols_Cons_index_0) finally show ?thesis . qed definition "lower_triangular A = (\i j. i < j \ i < dim_row A \ j < dim_col A \ A $$ (i,j) = 0)" lemma lower_triangular_index: assumes "lower_triangular A" "i carrier_mat n n" shows "A * (k \\<^sub>m (1\<^sub>m n)) = (k \\<^sub>m (1\<^sub>m n)) * A" proof - - have "(\ia = 0..ia = 0..ia = 0..ia \ ({0..ia \ ({0..ia \ ({0..ia \ ({0.. carrier_mat 2 2" shows "Determinant.det A = A$$(0,0) * A $$ (1,1) - A$$(0,1)*A$$(1,0)" proof - let ?A = "(Mod_Type_Connect.to_hma\<^sub>m A)::'a^2^2" - have [transfer_rule]: "Mod_Type_Connect.HMA_M A ?A" + have [transfer_rule]: "Mod_Type_Connect.HMA_M A ?A" unfolding Mod_Type_Connect.HMA_M_def using from_hma_to_hma\<^sub>m A by auto have [transfer_rule]: "Mod_Type_Connect.HMA_I 0 0" unfolding Mod_Type_Connect.HMA_I_def by (simp add: to_nat_0) have [transfer_rule]: "Mod_Type_Connect.HMA_I 1 1" unfolding Mod_Type_Connect.HMA_I_def by (simp add: to_nat_1) have "Determinant.det A = Determinants.det ?A" by (transfer, simp) also have "... = ?A $h 1 $h 1 * ?A $h 2 $h 2 - ?A $h 1 $h 2 * ?A $h 2 $h 1" unfolding det_2 by simp also have "... = ?A $h 0 $h 0 * ?A $h 1 $h 1 - ?A $h 0 $h 1 * ?A $h 1 $h 0" by (smt Groups.mult_ac(2) exhaust_2 semiring_norm(160)) - also have "... = A$$(0,0) * A $$ (1,1) - A$$(0,1)*A$$(1,0)" + also have "... = A$$(0,0) * A $$ (1,1) - A$$(0,1)*A$$(1,0)" unfolding index_hma_def[symmetric] by (transfer, auto) finally show ?thesis . qed lemma mat_diag_smult: "mat_diag n (\ x. (k::'a::comm_ring_1)) = (k \\<^sub>m 1\<^sub>m n)" proof - have "mat_diag n (\ x. k) = mat_diag n (\ x. k * 1)" by auto also have "... = mat_diag n (\ x. k) * mat_diag n (\ x. 1)" using mat_diag_diag by (simp add: mat_diag_def) also have "... = mat_diag n (\ x. k) * (1\<^sub>m n)" by auto thm mat_diag_mult_left also have "... = Matrix.mat n n (\(i, j). k * (1\<^sub>m n) $$ (i, j))" by (rule mat_diag_mult_left, auto) also have "... = (k \\<^sub>m 1\<^sub>m n)" unfolding smult_mat_def by auto finally show ?thesis . qed lemma invertible_mat_four_block_mat_lower_right: assumes A: "(A::'a::comm_ring_1 mat) \ carrier_mat n n" and inv_A: "invertible_mat A" shows "invertible_mat (four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 n) (0\<^sub>m n 1) A)" proof - let ?I = "(four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 n) (0\<^sub>m n 1) A)" - have "Determinant.det ?I = Determinant.det (1\<^sub>m 1) * Determinant.det A" + have "Determinant.det ?I = Determinant.det (1\<^sub>m 1) * Determinant.det A" by (rule det_four_block_mat_lower_left_zero_col, insert assms, auto) also have "... = Determinant.det A" by auto finally have "Determinant.det ?I = Determinant.det A" . thus ?thesis - by (metis (no_types, lifting) assms carrier_matD(1) carrier_matD(2) carrier_mat_triv - index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3) + by (metis (no_types, lifting) assms carrier_matD(1) carrier_matD(2) carrier_mat_triv + index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3) invertible_iff_is_unit_JNF) qed lemma invertible_mat_four_block_mat_lower_right_id: assumes A: "(A::'a::comm_ring_1 mat) \ carrier_mat m m" and B: "B = 0\<^sub>m m (n-m)" and C: "C = 0\<^sub>m (n-m) m" and D: "D = 1\<^sub>m (n-m)" and "n>m" and inv_A: "invertible_mat A" shows "invertible_mat (four_block_mat A B C D)" proof - have "Determinant.det (four_block_mat A B C D) = Determinant.det A" by (rule det_four_block_mat_lower_right_id, insert assms, auto) thus ?thesis using inv_A - by (metis (no_types, lifting) assms(1) assms(4) carrier_matD(1) carrier_matD(2) carrier_mat_triv - index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3) + by (metis (no_types, lifting) assms(1) assms(4) carrier_matD(1) carrier_matD(2) carrier_mat_triv + index_mat_four_block(2) index_mat_four_block(3) index_one_mat(2) index_one_mat(3) invertible_iff_is_unit_JNF) qed lemma split_block4_decreases_dim_row: - assumes E: "(A,B,C,D) = split_block E 1 1" + assumes E: "(A,B,C,D) = split_block E 1 1" and E1: "dim_row E > 1" and E2: "dim_col E > 1" shows "dim_row D < dim_row E" proof - have "D \ carrier_mat (1 + (dim_row E - 2)) (1 + (dim_col E - 2))" by (rule split_block(4)[OF E[symmetric]], insert E1 E2, auto) hence "D \ carrier_mat (dim_row E - 1) (dim_col E - 1)" using E1 E2 by auto thus ?thesis using E1 by auto qed lemma inv_P'PAQQ': - assumes A: "A \ carrier_mat n n" - and P: "P \ carrier_mat n n" - and inv_P: "inverts_mat P' P" + assumes A: "A \ carrier_mat n n" + and P: "P \ carrier_mat n n" + and inv_P: "inverts_mat P' P" and inv_Q: "inverts_mat Q Q'" - and Q: "Q \ carrier_mat n n" - and P': "P' \ carrier_mat n n" + and Q: "Q \ carrier_mat n n" + and P': "P' \ carrier_mat n n" and Q': "Q' \ carrier_mat n n" shows "(P'*(P*A*Q)*Q') = A" proof - have "(P'*(P*A*Q)*Q') = (P'*(P*A*Q*Q'))" - by (smt P P' Q Q' assoc_mult_mat carrier_matD(1) carrier_matD(2) carrier_mat_triv + by (smt P P' Q Q' assoc_mult_mat carrier_matD(1) carrier_matD(2) carrier_mat_triv index_mult_mat(2) index_mult_mat(3)) also have "... = ((P'*P)*A*(Q*Q'))" - by (smt A P P' Q Q' assoc_mult_mat carrier_matD(1) carrier_matD(2) carrier_mat_triv - index_mult_mat(3) inv_Q inverts_mat_def right_mult_one_mat') - finally show ?thesis - by (metis P' Q A inv_P inv_Q carrier_matD(1) inverts_mat_def + by (smt A P P' Q Q' assoc_mult_mat carrier_matD(1) carrier_matD(2) carrier_mat_triv + index_mult_mat(3) inv_Q inverts_mat_def right_mult_one_mat') + finally show ?thesis + by (metis P' Q A inv_P inv_Q carrier_matD(1) inverts_mat_def left_mult_one_mat right_mult_one_mat) qed -lemma +lemma assumes "U \ carrier_mat 2 2" and "V \ carrier_mat 2 2" and "A = U * V" shows mat_mult2_00: "A $$ (0,0) = U $$ (0,0)*V $$ (0,0) + U $$ (0,1)*V $$ (1,0)" and mat_mult2_01: "A $$ (0,1) = U $$ (0,0)*V $$ (0,1) + U $$ (0,1)*V $$ (1,1)" and mat_mult2_10: "A $$ (1,0) = U $$ (1,0)*V $$ (0,0) + U $$ (1,1)*V $$ (1,0)" and mat_mult2_11: "A $$ (1,1) = U $$ (1,0)*V $$ (0,1) + U $$ (1,1)*V $$ (1,1)" using assms unfolding times_mat_def Matrix.row_def col_def scalar_prod_def using sum_two_rw by auto subsection\Lemmas about @{text "sorted lists"}, @{text "insort"} and @{text "pick"}\ lemma sorted_distinct_imp_sorted_wrt: assumes "sorted xs" and "distinct xs" - shows "sorted_wrt (<) xs" - using assms + shows "sorted_wrt (<) xs" + using assms by (induct xs, insert le_neq_trans, auto) lemma sorted_map_strict: assumes "strict_mono_on g {0.. g ` {0..x\set (map g [0.. g n" using sg unfolding strict_mono_on_def + show "\x\set (map g [0.. g n" using sg unfolding strict_mono_on_def by (simp add: less_imp_le) qed finally show ?case . qed lemma sorted_nth_strict_mono: "sorted xs \ distinct xs \i < j \ j < length xs \ xs!i < xs!j" by (simp add: less_le nth_eq_iff_index_eq sorted_iff_nth_mono_less) lemma sorted_list_of_set_0_LEAST: assumes finI: "finite I" and I: "I \ {}" shows "sorted_list_of_set I ! 0 = (LEAST n. n\I)" proof (rule Least_equality[symmetric]) show "sorted_list_of_set I ! 0 \ I" by (metis I Max_in finI gr_zeroI in_set_conv_nth not_less_zero set_sorted_list_of_set) fix y assume "y \ I" thus "sorted_list_of_set I ! 0 \ y" - by (metis eq_iff finI in_set_conv_nth neq0_conv sorted_iff_nth_mono_less + by (metis eq_iff finI in_set_conv_nth neq0_conv sorted_iff_nth_mono_less sorted_list_of_set(1) sorted_sorted_list_of_set) qed lemma sorted_list_of_set_eq_pick: - assumes i: "i < length (sorted_list_of_set I)" + assumes i: "i < length (sorted_list_of_set I)" shows "sorted_list_of_set I ! i = pick I i" -proof - - have finI: "finite I" +proof - + have finI: "finite I" proof (rule ccontr) assume "infinite I" hence "length (sorted_list_of_set I) = 0" using sorted_list_of_set.infinite by auto thus False using i by simp qed - show ?thesis + show ?thesis using i proof (induct i) case 0 have I: "I \ {}" using "0.prems" sorted_list_of_set_empty by blast show ?case unfolding pick.simps by (rule sorted_list_of_set_0_LEAST[OF finI I]) next case (Suc i) note x_less = Suc.prems show ?case proof (unfold pick.simps, rule Least_equality[symmetric], rule conjI) show 1: "pick I i < sorted_list_of_set I ! Suc i" by (metis Suc.hyps Suc.prems Suc_lessD distinct_sorted_list_of_set find_first_unique lessI nat_less_le sorted_sorted_list_of_set sorted_sorted_wrt sorted_wrt_nth_less) show "sorted_list_of_set I ! Suc i \ I" using Suc.prems finI nth_mem set_sorted_list_of_set by blast - have rw: "sorted_list_of_set I ! i = pick I i" - by (rule Suc.hyps, simp add: Suc.prems Suc_lessD) - have sorted_less: "sorted_list_of_set I ! i < sorted_list_of_set I ! Suc i" + have rw: "sorted_list_of_set I ! i = pick I i" + using Suc.hyps Suc_lessD x_less by blast + have sorted_less: "sorted_list_of_set I ! i < sorted_list_of_set I ! Suc i" by (simp add: 1 rw) fix y assume y: "y \ I \ pick I i < y" - show "sorted_list_of_set I ! Suc i \ y" - by (smt antisym_conv finI in_set_conv_nth less_Suc_eq less_Suc_eq_le nat_neq_iff rw + show "sorted_list_of_set I ! Suc i \ y" + by (smt antisym_conv finI in_set_conv_nth less_Suc_eq less_Suc_eq_le nat_neq_iff rw sorted_iff_nth_mono_less sorted_list_of_set(1) sorted_sorted_list_of_set x_less y) - qed + qed qed qed -text\$b$ is the position where we add, $a$ the element to be added and $i$ the position +text\$b$ is the position where we add, $a$ the element to be added and $i$ the position that is checked\ lemma insort_nth': - assumes "\j set xs" - and "i < length xs + 1" and "i < b" + assumes "\j set xs" + and "i < length xs + 1" and "i < b" and "xs \ []" and "b < length xs" shows "insort a xs ! i = xs ! i" using assms proof (induct xs arbitrary: a b i) case Nil then show ?case by auto next case (Cons x xs) note less = Cons.prems(1) note sorted = Cons.prems(2) note a_notin = Cons.prems(3) note i_length = Cons.prems(4) note i_b = Cons.prems(5) note b_length = Cons.prems(7) show ?case proof (cases "a \ x") case True have "insort a (x # xs) ! i = (a # x # xs) ! i" using True by simp also have "... = (x # xs) ! i" using Cons.prems(1) Cons.prems(5) True by force finally show ?thesis . next case False note x_less_a = False have "insort a (x # xs) ! i = (x # insort a xs) ! i" using False by simp also have "... = (x # xs) ! i" proof (cases "i = 0") case True then show ?thesis by auto next case False have "(x # insort a xs) ! i = (insort a xs) ! (i-1)" by (simp add: False nth_Cons') also have "... = xs ! (i-1)" proof (rule Cons.hyps) show "sorted xs" using sorted by simp show "a \ set xs" using a_notin by simp show "i - 1 < length xs + 1" using i_length False by auto show "xs \ []" using i_b b_length by force show "i - 1 < b - 1" by (simp add: False diff_less_mono i_b leI) show "b - 1 < length xs" using b_length i_b by auto show "\j set xs" - and "i < index (insort a xs) a" + assumes "sorted xs" and "a \ set xs" + and "i < index (insort a xs) a" and "xs \ []" shows "insort a xs ! i = xs ! i" using assms proof (induct xs arbitrary: a i) case Nil then show ?case by auto next case (Cons x xs) note sorted = Cons.prems(1) note a_notin = Cons.prems(2) - note i_index = Cons.prems(3) + note i_index = Cons.prems(3) show ?case proof (cases "a \ x") case True have "insort a (x # xs) ! i = (a # x # xs) ! i" using True by simp also have "... = (x # xs) ! i" using Cons.prems(1) Cons.prems(3) True by force finally show ?thesis . next case False note x_less_a = False - show ?thesis + show ?thesis proof (cases "xs = []") case True have "x \ a" using False by auto then show ?thesis using True i_index False by auto next - case False note xs_not_empty = False + case False note xs_not_empty = False have "insort a (x # xs) ! i = (x # insort a xs) ! i" using x_less_a by simp also have "... = (x # xs) ! i" proof (cases "i = 0") case True then show ?thesis by auto next case False note i0 = False have "(x # insort a xs) ! i = (insort a xs) ! (i-1)" by (simp add: False nth_Cons') also have "... = xs ! (i-1)" proof (rule Cons.hyps[OF _ _ _ xs_not_empty]) show "sorted xs" using sorted by simp show "a \ set xs" using a_notin by simp - have "index (insort a (x # xs)) a = index ((x # insort a xs)) a" + have "index (insort a (x # xs)) a = index ((x # insort a xs)) a" using x_less_a by auto - also have "... = index (insort a xs) a + 1" + also have "... = index (insort a xs) a + 1" unfolding index_Cons using x_less_a by simp finally show "i - 1 < index (insort a xs) a" using False i_index by linarith qed also have "... = (x # xs) ! i" by (simp add: False nth_Cons') finally show ?thesis . qed finally show ?thesis . qed qed qed lemma insort_nth2: - assumes "sorted xs" and "a \ set xs" - and "i < length xs" and "i \ index (insort a xs) a" + assumes "sorted xs" and "a \ set xs" + and "i < length xs" and "i \ index (insort a xs) a" and "xs \ []" shows "insort a xs ! (Suc i) = xs ! i" using assms proof (induct xs arbitrary: a i) case Nil then show ?case by auto next case (Cons x xs) note sorted = Cons.prems(1) note a_notin = Cons.prems(2) note i_length = Cons.prems(3) note index_i = Cons.prems(4) show ?case proof (cases "a \ x") case True have "insort a (x # xs) ! (Suc i) = (a # x # xs) ! (Suc i)" using True by simp also have "... = (x # xs) ! i" using Cons.prems(1) Cons.prems(5) True by force finally show ?thesis . next case False note x_less_a = False have "insort a (x # xs) ! (Suc i) = (x # insort a xs) ! (Suc i)" using False by simp also have "... = (x # xs) ! i" proof (cases "i = 0") case True then show ?thesis using index_i linear x_less_a by fastforce next case False note i0 = False show ?thesis - proof - + proof - have Suc_i: "Suc (i - 1) = i" using i0 by auto have "(x # insort a xs) ! (Suc i) = (insort a xs) ! i" by (simp add: nth_Cons') also have "... = (insort a xs) ! Suc (i - 1)" using Suc_i by simp also have "... = xs ! (i - 1)" proof (rule Cons.hyps) show "sorted xs" using sorted by simp show "a \ set xs" using a_notin by simp show "i - 1 < length xs" using i_length using Suc_i by auto - thus "xs \ []" by auto + thus "xs \ []" by auto have "index (insort a (x # xs)) a = index ((x # insort a xs)) a" using x_less_a by simp also have "... = index (insort a xs) a + 1" unfolding index_Cons using x_less_a by simp finally show "index (insort a xs) a \ i - 1" using index_i i0 by auto qed also have "... = (x # xs) ! i" using Suc_i by auto finally show ?thesis . qed qed finally show ?thesis . qed qed lemma pick_index: assumes a: "a \ I" and a'_card: "a' < card I" shows "(pick I a' = a) = (index (sorted_list_of_set I) a = a')" proof - have finI: "finite I" using a'_card card_infinite by force have length_I: "length (sorted_list_of_set I) = card I" by (metis a'_card card_infinite distinct_card distinct_sorted_list_of_set not_less_zero set_sorted_list_of_set) let ?i = "index (sorted_list_of_set I) a" have "(sorted_list_of_set I) ! a' = pick I a'" by (rule sorted_list_of_set_eq_pick, auto simp add: finI a'_card length_I) moreover have "(sorted_list_of_set I) ! ?i = a" by (rule nth_index, simp add: a finI) ultimately show ?thesis by (metis a'_card distinct_sorted_list_of_set index_nth_id length_I) qed end diff --git a/thys/Smith_Normal_Form/SNF_Uniqueness.thy b/thys/Smith_Normal_Form/SNF_Uniqueness.thy --- a/thys/Smith_Normal_Form/SNF_Uniqueness.thy +++ b/thys/Smith_Normal_Form/SNF_Uniqueness.thy @@ -1,1180 +1,1180 @@ (* Author: Jose Divasón - Email: jose.divason@unirioja.es + Email: jose.divason@unirioja.es *) section \Uniqueness of the Smith normal form\ theory SNF_Uniqueness imports Cauchy_Binet - Smith_Normal_Form_JNF + Smith_Normal_Form_JNF Admits_SNF_From_Diagonal_Iff_Bezout_Ring -begin +begin lemma dvd_associated1: fixes a::"'a::comm_ring_1" assumes "\u. u dvd 1 \ a = u*b" shows "a dvd b \ b dvd a" using assms by auto -text \This is a key lemma. It demands the type class to be an integral domain. This means that +text \This is a key lemma. It demands the type class to be an integral domain. This means that the uniqueness result will be obtained for GCD domains, instead of rings.\ lemma dvd_associated2: fixes a::"'a::idom" assumes ab: "a dvd b" and ba: "b dvd a" and a: "a\0" shows "\u. u dvd 1 \ a = u*b" proof - obtain k where a_kb: "a = k*b" using ab unfolding dvd_def by (metis Groups.mult_ac(2) ba dvdE) - obtain q where b_qa: "b = q*a" using ba unfolding dvd_def + obtain q where b_qa: "b = q*a" using ba unfolding dvd_def by (metis Groups.mult_ac(2) ab dvdE) - have 1: "a = k*q*a" using a_kb b_qa by auto + have 1: "a = k*q*a" using a_kb b_qa by auto hence "k*q = 1" using a by simp thus ?thesis using 1 by (metis a_kb dvd_triv_left) qed corollary dvd_associated: fixes a::"'a::idom" assumes "a\0" shows "(a dvd b \ b dvd a) = (\u. u dvd 1 \ a = u*b)" using assms dvd_associated1 dvd_associated2 by metis lemma exists_inj_ge_index: assumes S: "S \ {0..f. inj_on f {0.. f`{0.. (\i\{0.. f i)" proof - have "\h. bij_betw h {0..i\{0.. ?f i" proof fix i assume i: "i \ {0.. ?xs ! i" + moreover have "i \ ?xs ! i" proof (rule sorted_wrt_less_idx, rule sorted_distinct_imp_sorted_wrt) show "sorted ?xs" using sorted_sorted_list_of_set by blast show "distinct ?xs" using distinct_sorted_list_of_set by blast show "i < length ?xs" by (metis S Sk atLeast0LessThan distinct_card distinct_sorted_list_of_set gk_S i lessThan_iff set_sorted_list_of_set subset_eq_atLeast0_lessThan_finite) qed ultimately show "i \ ?f i" by auto qed show ?thesis using 1 2 3 by auto qed subsection \More specific results about submatrices\ lemma diagonal_imp_submatrix0: assumes dA: "diagonal_mat A" and A_carrier: "A\ carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" + and Ik: "card I = k" and Jk: "card J = k" and r: "\row_index \ I. row_index < n" (*I \ {0..col_index \ J. col_index < m" and a: "a submatrix A I J $$ (a,b) = A $$(pick I a, pick I a)" proof (cases "submatrix A I J $$ (a, b) = 0") case True then show ?thesis by auto next case False note not0 = False have aux: "submatrix A I J $$ (a, b) = A $$(pick I a, pick J b)" proof (rule submatrix_index) have "card {i. i < dim_row A \ i \ I} = k" by (smt A_carrier Ik carrier_matD(1) equalityI mem_Collect_eq r subsetI) - moreover have "card {i. i < dim_col A \ i \ J} = k" - by (metis (no_types, lifting) A_carrier Jk c carrier_matD(2) carrier_mat_def + moreover have "card {i. i < dim_col A \ i \ J} = k" + by (metis (no_types, lifting) A_carrier Jk c carrier_matD(2) carrier_mat_def equalityI mem_Collect_eq subsetI) - ultimately show " a < card {i. i < dim_row A \ i \ I}" + ultimately show " a < card {i. i < dim_row A \ i \ I}" and "b < card {i. i < dim_col A \ i \ J}" using a b by auto qed thus ?thesis proof (cases "pick I a = pick J b") case True then show ?thesis using aux by auto next case False - then show ?thesis + then show ?thesis by (metis aux A_carrier Ik Jk a b c carrier_matD dA diagonal_mat_def pick_in_set_le r) qed qed lemma diagonal_imp_submatrix_element_not0: assumes dA: "diagonal_mat A" and A_carrier: "A \ carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" + and Ik: "card I = k" and Jk: "card J = k" and I: "I \ {0.. {0..i. i submatrix A I J $$ (i, b) \ 0" shows "\!i. i submatrix A I J $$ (i, b) \ 0" proof - have I_eq: "I = {i. i < dim_row A \ i \ I}" using I A_carrier unfolding carrier_mat_def by auto have J_eq: "J = {i. i < dim_col A \ i \ J}" using J A_carrier unfolding carrier_mat_def by auto - obtain a where sub_ab: "submatrix A I J $$ (a, b) \ 0" and ak: "a < k" using ex_not0 by auto + obtain a where sub_ab: "submatrix A I J $$ (a, b) \ 0" and ak: "a < k" using ex_not0 by auto moreover have "i = a" if sub_ib: "submatrix A I J $$ (i, b) \ 0" and ik: "i < k" for i proof - have 1: "pick I i < dim_row A" using I_eq Ik ik pick_in_set_le by auto have 2: "pick J b < dim_col A" using J_eq Jk b pick_le by auto have 3: "pick I a < dim_row A" using I_eq Ik calculation(2) pick_le by auto have "submatrix A I J $$ (i, b) = A $$ (pick I i, pick J b)" by (rule submatrix_index, insert I_eq Ik ik J_eq Jk b, auto) hence pick_Ii_Jb: "pick I i = pick J b" using dA sub_ib 1 2 unfolding diagonal_mat_def by auto have "submatrix A I J $$ (a, b) = A $$ (pick I a, pick J b)" by (rule submatrix_index, insert I_eq Ik ak J_eq Jk b, auto) hence pick_Ia_Jb: "pick I a = pick J b" using dA sub_ab 3 2 unfolding diagonal_mat_def by auto have pick_Ia_Ii: "pick I a = pick I i" using pick_Ii_Jb pick_Ia_Jb by simp - thus ?thesis by (metis Ik ak ik nat_neq_iff pick_mono_le) + thus ?thesis by (metis Ik ak ik nat_neq_iff pick_mono_le) qed ultimately show ?thesis by auto qed -lemma submatrix_index_exists: +lemma submatrix_index_exists: assumes A_carrier: "A\ carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" + and Ik: "card I = k" and Jk: "card J = k" and a: "a \ I" and b: "b \ J" and k: "k > 0" and I: "I \ {0.. {0..a' b'. a' < k \ b' < k \ submatrix A I J $$ (a',b') = A $$ (a,b) +shows "\a' b'. a' < k \ b' < k \ submatrix A I J $$ (a',b') = A $$ (a,b) \ a = pick I a' \ b = pick J b'" proof - let ?xs = "sorted_list_of_set I" let ?ys = "sorted_list_of_set J" have finI: "finite I" and finJ: "finite J" using k Ik Jk card_ge_0_finite by metis+ - have set_xs: "set ?xs = I" by (rule set_sorted_list_of_set[OF finI]) + have set_xs: "set ?xs = I" by (rule set_sorted_list_of_set[OF finI]) have set_ys: "set ?ys = J" by (rule set_sorted_list_of_set[OF finJ]) have a_in_xs: "a \ set ?xs" and b_in_ys: "b \ set ?ys" using set_xs a set_ys b by auto have length_xs: "length ?xs = k" by (metis Ik distinct_card set_xs sorted_list_of_set(3)) have length_ys: "length ?ys = k" by (metis Jk distinct_card set_ys sorted_list_of_set(3)) - obtain a' where a': "?xs ! a' = a" and a'_length: "a' < length ?xs" + obtain a' where a': "?xs ! a' = a" and a'_length: "a' < length ?xs" by (meson a_in_xs in_set_conv_nth) - obtain b' where b': "?ys ! b' = b" and b'_length: "b' < length ?ys" + obtain b' where b': "?ys ! b' = b" and b'_length: "b' < length ?ys" by (meson b_in_ys in_set_conv_nth) have pick_a: "a = pick I a'" using a' a'_length finI sorted_list_of_set_eq_pick by auto have pick_b: "b = pick J b'" using b' b'_length finJ sorted_list_of_set_eq_pick by auto - have I_rw: "I = {i. i < dim_row A \ i \ I}" and J_rw: "J = {i. i < dim_col A \ i \ J}" + have I_rw: "I = {i. i < dim_row A \ i \ I}" and J_rw: "J = {i. i < dim_col A \ i \ J}" using I A_carrier J by auto have a'k: "a' < k" using a'_length length_xs by auto moreover have b'k: "b' carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" + and Ik: "card I = k" and Jk: "card J = k" and I: "I \ {0.. {0.. I" and b_notin_J: "b \ J" - and a'k: "a' < Suc k" and b'k: "b' < Suc k" + and a'k: "a' < Suc k" and b'k: "b' < Suc k" and a_def: "pick (insert a I) a' = a" and b_def: "pick (insert b J) b' = b" shows "mat_delete (submatrix A (insert a I) (insert b J)) a' b' = submatrix A I J" (is "?lhs = ?rhs") proof (rule eq_matI) have I_eq: "I = {i. i < dim_row A \ i \ I}" using I A_carrier unfolding carrier_mat_def by auto have J_eq: "J = {i. i < dim_col A \ i \ J}" using J A_carrier unfolding carrier_mat_def by auto - have insert_I_eq: "insert a I = {i. i < dim_row A \ i \ insert a I}" + have insert_I_eq: "insert a I = {i. i < dim_row A \ i \ insert a I}" using I A_carrier a k unfolding carrier_mat_def by auto - have card_Suc_k: "card {i. i < dim_row A \ i \ insert a I} = Suc k" + have card_Suc_k: "card {i. i < dim_row A \ i \ insert a I} = Suc k" using insert_I_eq Ik a_notin_I by (metis I card_insert_disjoint finite_atLeastLessThan finite_subset) - have insert_J_eq: "insert b J = {i. i < dim_col A \ i \ insert b J}" + have insert_J_eq: "insert b J = {i. i < dim_col A \ i \ insert b J}" using J A_carrier b k unfolding carrier_mat_def by auto - have card_Suc_k': "card {i. i < dim_col A \ i \ insert b J} = Suc k" + have card_Suc_k': "card {i. i < dim_col A \ i \ insert b J} = Suc k" using insert_J_eq Jk b_notin_J by (metis J card_insert_disjoint finite_atLeastLessThan finite_subset) show "dim_row ?lhs = dim_row ?rhs" unfolding mat_delete_dim unfolding dim_submatrix using card_Suc_k I_eq Ik by auto show "dim_col ?lhs = dim_col ?rhs" unfolding mat_delete_dim unfolding dim_submatrix using card_Suc_k' J_eq Jk by auto fix i j assume i: "i < dim_row (submatrix A I J)" and j: "j < dim_col (submatrix A I J)" have ik: "i < k" by (metis I_eq Ik dim_submatrix(1) i) have jk: "j < k" by (metis J_eq Jk dim_submatrix(2) j) show "?lhs $$ (i, j) = ?rhs $$ (i, j)" - proof - + proof - have index_eq1: "pick (insert a I) (insert_index a' i) = pick I i" by (rule pick_insert_index[OF Ik a_notin_I ik a_def], simp add: Ik a'k) have index_eq2: "pick (insert b J) (insert_index b' j) = pick J j" by (rule pick_insert_index[OF Jk b_notin_J jk b_def], simp add: Jk b'k) - have "?lhs $$ (i,j) + have "?lhs $$ (i,j) = (submatrix A (insert a I) (insert b J)) $$ (insert_index a' i, insert_index b' j)" proof (rule mat_delete_index[symmetric, OF _ a'k b'k ik jk]) show "submatrix A (insert a I) (insert b J) \ carrier_mat (Suc k) (Suc k)" by (metis card_Suc_k card_Suc_k' carrier_matI dim_submatrix(1) dim_submatrix(2)) qed - also have "... = A $$ (pick (insert a I) (insert_index a' i), pick (insert b J) (insert_index b' j))" + also have "... = A $$ (pick (insert a I) (insert_index a' i), pick (insert b J) (insert_index b' j))" proof (rule submatrix_index) show "insert_index a' i < card {i. i < dim_row A \ i \ insert a I}" using card_Suc_k ik insert_index_def by auto show "insert_index b' j < card {j. j < dim_col A \ j \ insert b J}" using card_Suc_k' insert_index_def jk by auto qed also have "... = A $$ (pick I i, pick J j)" unfolding index_eq1 index_eq2 by auto also have "... = submatrix A I J $$ (i,j)" - by (rule submatrix_index[symmetric], insert ik I_eq Ik Jk J_eq jk, auto) + by (rule submatrix_index[symmetric], insert ik I_eq Ik Jk J_eq jk, auto) finally show ?thesis . qed qed subsection \On the minors of a diagonal matrix\ lemma det_minors_diagonal: assumes dA: "diagonal_mat A" and A_carrier: "A \ carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" - and r: "I \ {0.. {0.. {0..0" - shows "det (submatrix A I J) = 0 - \ (\xs. (det (submatrix A I J) = prod_list xs \ det (submatrix A I J) = - prod_list xs) + shows "det (submatrix A I J) = 0 + \ (\xs. (det (submatrix A I J) = prod_list xs \ det (submatrix A I J) = - prod_list xs) \ set xs \ {A$$(i,i)|i. i A$$(i,i)\ 0} \ length xs = k)" using Ik Jk r c k proof (induct k arbitrary: I J) case 0 then show ?case by auto next case (Suc k) note cardI = Suc.prems(1) note cardJ = Suc.prems(2) note I = Suc.prems(3) note J = Suc.prems(4) have *: "{i. i < dim_row A \ i \ I} = I" using I Ik A_carrier carrier_mat_def by auto have **: "{j. j < dim_col A \ j \ J} = J" using J Jk A_carrier carrier_mat_def by auto show ?case proof (cases "k = 0") case True note k0 = True from this obtain a where aI: "I = {a}" using True cardI card_1_singletonE by auto from this obtain b where bJ: "J = {b}" using True cardJ card_1_singletonE by auto have an: "a carrier_mat 1 1" - unfolding carrier_mat_def submatrix_def + have sub_carrier: "submatrix A {a} {b} \ carrier_mat 1 1" + unfolding carrier_mat_def submatrix_def using * ** aI bJ by auto - have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)" + have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)" by (rule det_singleton[OF sub_carrier]) - have 2: "... = A $$ (a,b)" + have 2: "... = A $$ (a,b)" by (rule submatrix_singleton_index[OF A_carrier an bm]) - show ?thesis + show ?thesis proof (cases "A $$ (a,b) \ 0") let ?xs = "[submatrix A {a} {b} $$ (0,0)]" case True hence "a = b" using dA A_carrier an bm unfolding diagonal_mat_def carrier_mat_def by auto - hence "set ?xs \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" + hence "set ?xs \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" using 2 True an bm by auto moreover have "det (submatrix A {a} {b}) = prod_list ?xs" using 1 by auto moreover have "length ?xs = Suc k" using k0 by auto ultimately show ?thesis using an bm unfolding aI bJ by blast next case False then show ?thesis using 1 2 aI bJ by auto - qed + qed next - case False + case False hence k0: "0 < k" by simp have k: "k < min n m" - by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute - min_def not_less subset_eq_atLeast0_lessThan_card) - have subIJ_carrier: "(submatrix A I J) \ carrier_mat (Suc k) (Suc k)" + by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute + min_def not_less subset_eq_atLeast0_lessThan_card) + have subIJ_carrier: "(submatrix A I J) \ carrier_mat (Suc k) (Suc k)" unfolding carrier_mat_def using * ** cardI cardJ - unfolding submatrix_def by auto + unfolding submatrix_def by auto obtain b' where b'k: "b' < Suc k" by auto - let ?f="\i. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'" + let ?f="\i. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'" have det_rw: "det (submatrix A I J) = (\ia' 0") case True - obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') \ 0" + obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') \ 0" and a'k: "a' < Suc k" and unique: "\j. j submatrix A I J $$ (j,b') \ 0 \ j = a'" using diagonal_imp_submatrix_element_not0[OF dA A_carrier cardI cardJ I J b'k True] by auto have "submatrix A I J $$ (a', b') = A $$ (pick I a', pick J b')" by (rule submatrix_index, auto simp add: "*" a'k cardI "**" b'k cardJ) - from this obtain a b where an: "a < n" and bm: "b < m" - and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)" + from this obtain a b where an: "a < n" and bm: "b < m" + and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)" and pick_a: "pick I a' = a" and pick_b: "pick J b' = b" using * ** A_carrier a'k b'k cardI cardJ pick_le by fastforce obtain I' where aI': "I = insert a I'" and a_notin: "a \ I'" by (metis Set.set_insert a'k cardI pick_a pick_in_set_le) obtain J' where bJ': "J = insert b J'" and b_notin: "b \ J'" - by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le) + by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le) have Suc_k0: "0 < Suc k" by simp have aI: "a \ I" using aI' by auto have bJ: "b \ J" using bJ' by auto have cardI': "card I' = k" - by (metis aI' a_notin cardI card_infinite card_insert_disjoint + by (metis aI' a_notin cardI card_infinite card_insert_disjoint finite_insert nat.inject nat.simps(3)) have cardJ': "card J' = k" - by (metis bJ' b_notin cardJ card_infinite card_insert_disjoint + by (metis bJ' b_notin cardJ card_infinite card_insert_disjoint finite_insert nat.inject nat.simps(3)) have I': "I' \ {0.. {0.. - (\xs. (det (submatrix A I' J') = prod_list xs \ det (submatrix A I' J') = - prod_list xs) + (\xs. (det (submatrix A I' J') = prod_list xs \ det (submatrix A I' J') = - prod_list xs) \ set xs \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0} \ length xs = k)" proof (rule Suc.hyps[OF cardI' cardJ' _ _ k0]) show "I' \ {0.. {0..i det (submatrix A I' J') = - prod_list xs" + from this obtain xs where prod_list_xs: "det (submatrix A I' J') = prod_list xs + \ det (submatrix A I' J') = - prod_list xs" and xs: "set xs \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" and length_xs: "length xs = k" using det_sub_I'J' by blast let ?ys = "A$$(a,b) # xs" have length_ys: "length ?ys = Suc k" using length_xs by auto have a_eq_b: "a=b" using A_carrier an bm sub_IJ_0 sub_index dA unfolding diagonal_mat_def by auto have A_aa_in: "A$$(a,a) \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" using a_eq_b an bm sub_IJ_0 sub_index by auto have ys: "set ?ys \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" using xs A_aa_in a_eq_b by auto show ?thesis proof (cases "even (a'+b')") case True have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * det (submatrix A I' J')" using det_submatrix_IJ True by auto show ?thesis proof (cases "det (submatrix A I' J') = prod_list xs") case True - have "det (submatrix A I J) = prod_list ?ys" + have "det (submatrix A I J) = prod_list ?ys" using det_submatrix_IJ unfolding True by auto then show ?thesis using ys length_ys by blast next case False hence "det (submatrix A I' J') = - prod_list xs" using prod_list_xs by simp hence "det (submatrix A I J) = - prod_list ?ys" using det_submatrix_IJ by auto then show ?thesis using ys length_ys by blast - qed + qed next case False have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * - det (submatrix A I' J')" using det_submatrix_IJ False by auto show ?thesis proof (cases "det (submatrix A I' J') = prod_list xs") case True - have "det (submatrix A I J) = - prod_list ?ys" + have "det (submatrix A I J) = - prod_list ?ys" using det_submatrix_IJ unfolding True by auto then show ?thesis using ys length_ys by blast next case False hence "det (submatrix A I' J') = - prod_list xs" using prod_list_xs by simp hence "det (submatrix A I J) = prod_list ?ys" using det_submatrix_IJ by auto then show ?thesis using ys length_ys by blast qed qed - qed + qed next - case False + case False have "sum ?f {0.. {0.. {0.. J \ {0.. card I = k \ card J = k}" lemma Gcd_minors_dvd: fixes A::"'a::{semiring_Gcd,comm_ring_1} mat" assumes PAQ_B: "P * A * Q = B" - and P: "P \ carrier_mat m m" + and P: "P \ carrier_mat m m" and A: "A \ carrier_mat m n" - and Q: "Q \ carrier_mat n n" + and Q: "Q \ carrier_mat n n" and I: "I \ {0.. {0.. carrier_mat k n" proof - have "I = {i. i < dim_row P \ i \ I}" using P I A by auto hence "card {i. i < dim_row P \ i \ I} = k" using Ik by auto thus ?thesis using A unfolding submatrix_def by auto - qed + qed have subQ: "submatrix Q UNIV J \ carrier_mat n k" proof - have J_eq: "J = {j. j < dim_col Q \ j \ J}" using Q J A by auto hence "card {j. j < dim_col Q \ j \ J} = k" using Jk by auto - moreover have "card {i. i < dim_row Q \ i \ UNIV} = n" using Q by auto + moreover have "card {i. i < dim_row Q \ i \ UNIV} = n" using Q by auto ultimately show ?thesis unfolding submatrix_def by auto qed have sub_sub_PA: "(submatrix ?subPA UNIV I') = submatrix (P * A) I I'" for I' using submatrix_split2[symmetric] by auto have det_subPA_rw: "det (submatrix (P * A) I I') = (\J' | J' \ {0.. card J' = k. det ((submatrix P I J')) * det (submatrix A J' I'))" if I'1: "I' \ {0..C | C \ {0.. card C = k. det (submatrix (submatrix P I UNIV) UNIV C) * det (submatrix (submatrix A UNIV I') C UNIV))" proof (rule Cauchy_Binet) have "I = {i. i < dim_row P \ i \ I}" using P I A by auto thus "submatrix P I UNIV \ carrier_mat k m" using Ik P unfolding submatrix_def by auto have "I' = {j. j < dim_col A \ j \ I'}" using I'1 A by auto thus "submatrix A UNIV I' \ carrier_mat m k" using I'2 A unfolding submatrix_def by auto qed also have "... = (\J' | J' \ {0.. card J' = k. det (submatrix P I J') * det (submatrix A J' I'))" unfolding submatrix_split2[symmetric] submatrix_split[symmetric] by simp finally show ?thesis . qed have "det (submatrix B I J) = det (submatrix (P*A*Q) I J)" using PAQ_B by simp also have "... = det (?subPA * ?subQ)" unfolding submatrix_mult by auto - also have "... = (\I' | I' \ {0.. card I' = k. det (submatrix ?subPA UNIV I') + also have "... = (\I' | I' \ {0.. card I' = k. det (submatrix ?subPA UNIV I') * det (submatrix ?subQ I' UNIV))" by (rule Cauchy_Binet[OF subPA subQ]) also have "... = (\I' | I' \ {0.. card I' = k. det (submatrix (P * A) I I') * det (submatrix Q I' J))" using submatrix_split[symmetric, of Q] submatrix_split2[symmetric, of "P*A"] by presburger also have "... = (\I' | I' \ {0.. card I' = k. \J' | J' \ {0.. card J' = k. det (submatrix P I J') * det (submatrix A J' I') * det (submatrix Q I' J))" using det_subPA_rw by (simp add: semiring_0_class.sum_distrib_right) - finally have det_rw: "det (submatrix B I J) = (\I' | I' \ {0.. card I' = k. + finally have det_rw: "det (submatrix B I J) = (\I' | I' \ {0.. card I' = k. \J' | J' \ {0.. card J' = k. det (submatrix P I J') * det (submatrix A J' I') * det (submatrix Q I' J))" . show ?thesis proof (unfold det_rw, (rule dvd_sum)+) fix I' J' assume I': "I' \ {I'. I' \ {0.. card I' = k}" and J': "J' \ {J'. J' \ {0.. card J' = k}" - have "Gcd (minors A k) dvd det (submatrix A J' I')" + have "Gcd (minors A k) dvd det (submatrix A J' I')" by (rule Gcd_dvd, unfold minors_def, insert A I' J', auto) - then show "Gcd (minors A k) dvd det (submatrix P I J') * det (submatrix A J' I') + then show "Gcd (minors A k) dvd det (submatrix P I J') * det (submatrix A J' I') * det (submatrix Q I' J)" by auto qed qed (*The conclusion could be simplified since we have S = I.*) lemma det_minors_diagonal2: assumes dA: "diagonal_mat A" and A_carrier: "A \ carrier_mat n m" - and Ik: "card I = k" and Jk: "card J = k" - and r: "I \ {0.. {0.. {0..0" shows "det (submatrix A I J) = 0 \ (\S. S \ {0.. card S = k \ S=I \ (det (submatrix A I J) = (\i\S. A $$ (i,i)) \ det (submatrix A I J) = - (\i\S. A $$ (i,i))))" using Ik Jk r c k proof (induct k arbitrary: I J) case 0 then show ?case by auto next case (Suc k) note cardI = Suc.prems(1) note cardJ = Suc.prems(2) note I = Suc.prems(3) note J = Suc.prems(4) have *: "{i. i < dim_row A \ i \ I} = I" using I Ik A_carrier carrier_mat_def by auto have **: "{j. j < dim_col A \ j \ J} = J" using J Jk A_carrier carrier_mat_def by auto show ?case proof (cases "k = 0") case True note k0 = True from this obtain a where aI: "I = {a}" using True cardI card_1_singletonE by auto from this obtain b where bJ: "J = {b}" using True cardJ card_1_singletonE by auto have an: "a carrier_mat 1 1" - unfolding carrier_mat_def submatrix_def + have sub_carrier: "submatrix A {a} {b} \ carrier_mat 1 1" + unfolding carrier_mat_def submatrix_def using * ** aI bJ by auto - have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)" + have 1: "det (submatrix A {a} {b}) = (submatrix A {a} {b}) $$ (0,0)" by (rule det_singleton[OF sub_carrier]) - have 2: "... = A $$ (a,b)" + have 2: "... = A $$ (a,b)" by (rule submatrix_singleton_index[OF A_carrier an bm]) - show ?thesis + show ?thesis proof (cases "A $$ (a,b) \ 0") let ?S="{a}" case True hence ab: "a = b" using dA A_carrier an bm unfolding diagonal_mat_def carrier_mat_def by auto hence "?S \ {0..i\?S. A $$ (i, i))" using 1 2 ab by auto moreover have "card ?S = Suc k" using k0 by auto ultimately show ?thesis using an bm unfolding aI bJ by blast next case False then show ?thesis using 1 2 aI bJ by auto - qed + qed next case False hence k0: "0 < k" by simp have k: "k < min n m" - by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute - min_def not_less subset_eq_atLeast0_lessThan_card) - have subIJ_carrier: "(submatrix A I J) \ carrier_mat (Suc k) (Suc k)" + by (metis I J cardI cardJ le_imp_less_Suc less_Suc_eq_le min.commute + min_def not_less subset_eq_atLeast0_lessThan_card) + have subIJ_carrier: "(submatrix A I J) \ carrier_mat (Suc k) (Suc k)" unfolding carrier_mat_def using * ** cardI cardJ - unfolding submatrix_def by auto + unfolding submatrix_def by auto obtain b' where b'k: "b' < Suc k" by auto - let ?f="\i. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'" + let ?f="\i. submatrix A I J $$ (i, b') * cofactor (submatrix A I J) i b'" have det_rw: "det (submatrix A I J) = (\ia' 0") case True - obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') \ 0" + obtain a' where sub_IJ_0: "submatrix A I J $$ (a',b') \ 0" and a'k: "a' < Suc k" and unique: "\j. j submatrix A I J $$ (j,b') \ 0 \ j = a'" using diagonal_imp_submatrix_element_not0[OF dA A_carrier cardI cardJ I J b'k True] by auto have "submatrix A I J $$ (a', b') = A $$ (pick I a', pick J b')" by (rule submatrix_index, auto simp add: "*" a'k cardI "**" b'k cardJ) - from this obtain a b where an: "a < n" and bm: "b < m" - and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)" + from this obtain a b where an: "a < n" and bm: "b < m" + and sub_index: "submatrix A I J $$ (a', b') = A $$ (a, b)" and pick_a: "pick I a' = a" and pick_b: "pick J b' = b" using * ** A_carrier a'k b'k cardI cardJ pick_le by fastforce obtain I' where aI': "I = insert a I'" and a_notin: "a \ I'" by (metis Set.set_insert a'k cardI pick_a pick_in_set_le) obtain J' where bJ': "J = insert b J'" and b_notin: "b \ J'" - by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le) + by (metis Set.set_insert b'k cardJ pick_b pick_in_set_le) have Suc_k0: "0 < Suc k" by simp have aI: "a \ I" using aI' by auto have bJ: "b \ J" using bJ' by auto have cardI': "card I' = k" - by (metis aI' a_notin cardI card_infinite card_insert_disjoint + by (metis aI' a_notin cardI card_infinite card_insert_disjoint finite_insert nat.inject nat.simps(3)) have cardJ': "card J' = k" - by (metis bJ' b_notin cardJ card_infinite card_insert_disjoint + by (metis bJ' b_notin cardJ card_infinite card_insert_disjoint finite_insert nat.inject nat.simps(3)) have I': "I' \ {0.. {0.. (\S\{0.. S=I' - \ (det (submatrix A I' J') = (\i\S. A $$ (i, i)) + \ (det (submatrix A I' J') = (\i\S. A $$ (i, i)) \ det (submatrix A I' J') = - (\i\S. A $$ (i, i))))" proof (rule Suc.hyps[OF cardI' cardJ' _ _ k0]) show "I' \ {0.. {0..ii\xs. A $$ (i, i)) - \ det (submatrix A I' J') = - (\i\xs. A $$ (i, i))" + from this obtain xs where prod_list_xs: "det (submatrix A I' J') = (\i\xs. A $$ (i, i)) + \ det (submatrix A I' J') = - (\i\xs. A $$ (i, i))" and xs: "xs\{0.. xs" by (simp add: xs_I' a_notin) have length_ys: "card ?ys = Suc k" using length_xs a_notin_xs by (simp add: card_ge_0_finite k0) have a_eq_b: "a=b" using A_carrier an bm sub_IJ_0 sub_index dA unfolding diagonal_mat_def by auto have A_aa_in: "A$$(a,a) \ {A $$ (i, i) |i. i < min n m \ A $$ (i, i) \ 0}" using a_eq_b an bm sub_IJ_0 sub_index by auto show ?thesis proof (cases "even (a'+b')") case True have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * det (submatrix A I' J')" using det_submatrix_IJ True by auto show ?thesis proof (cases "det (submatrix A I' J') = (\i\xs. A $$ (i, i))") case True - have "det (submatrix A I J) = (\i\?ys. A $$ (i, i))" + have "det (submatrix A I J) = (\i\?ys. A $$ (i, i))" using det_submatrix_IJ unfolding True a_eq_b - by (metis (no_types, lifting) a_notin_xs a_eq_b + by (metis (no_types, lifting) a_notin_xs a_eq_b card_ge_0_finite k0 length_xs prod.insert) then show ?thesis using length_ys using a_eq_b an bm xs xs_I' by (simp add: aI') next case False hence "det (submatrix A I' J') = - (\i\xs. A $$ (i, i))" using prod_list_xs by simp hence "det (submatrix A I J) = -(\i\?ys. A $$ (i, i))" using det_submatrix_IJ a_eq_b - by (metis (no_types, lifting) a_notin_xs card_ge_0_finite k0 + by (metis (no_types, lifting) a_notin_xs card_ge_0_finite k0 length_xs mult_minus_right prod.insert) then show ?thesis using length_ys using a_eq_b an bm xs aI' xs_I' by force - qed + qed next case False have det_submatrix_IJ: "det (submatrix A I J) = A $$ (a, b) * - det (submatrix A I' J')" using det_submatrix_IJ False by auto show ?thesis proof (cases "det (submatrix A I' J') = (\i\xs. A $$ (i, i))") case True - have "det (submatrix A I J) = - (\i\?ys. A $$ (i, i))" + have "det (submatrix A I J) = - (\i\?ys. A $$ (i, i))" using det_submatrix_IJ unfolding True - by (metis (no_types, lifting) a_eq_b a_notin_xs card_ge_0_finite k0 + by (metis (no_types, lifting) a_eq_b a_notin_xs card_ge_0_finite k0 length_xs mult_minus_right prod.insert) then show ?thesis using length_ys using a_eq_b an bm xs aI' xs_I' by force next case False hence "det (submatrix A I' J') = - (\i\xs. A $$ (i, i))" using prod_list_xs by simp hence "det (submatrix A I J) = (\i\?ys. A $$ (i, i))" using det_submatrix_IJ - by (metis (mono_tags, lifting) a_eq_b a_notin_xs card_ge_0_finite + by (metis (mono_tags, lifting) a_eq_b a_notin_xs card_ge_0_finite equation_minus_iff k0 length_xs prod.insert) - then show ?thesis using length_ys + then show ?thesis using length_ys using a_eq_b an bm xs aI' xs_I' by force qed qed - qed + qed next - case False + case False have "sum ?f {0..Relating minors and GCD\ lemma diagonal_dvd_Gcd_minors: fixes A::"'a::{semiring_Gcd,comm_ring_1} mat" - assumes A: "A \ carrier_mat n m" + assumes A: "A \ carrier_mat n m" and SNF_A: "Smith_normal_form_mat A" shows "(\i=0.. minors A k" show "(\i = 0.. {0.. {0.. {0.. {0..i\S. A $$ (i,i)) + and det_subS: "det (submatrix A I J) = (\i\S. A $$ (i,i)) \ det (submatrix A I J) = -(\i\S. A $$ (i,i))" using det_minors_diagonal2[OF diag_A A Ik Jk _ _ k] I J A False b by auto - obtain f where inj_f: "inj_on f {0..i\{0.. f i)" using exists_inj_ge_index[OF S Sk] by blast - have "(\i = 0..i\{0..i\f`{0..i = 0..i\{0..i\f`{0..i\S. A $$ (i, i))" using fk_S by auto - finally have *: "(\i = 0..i\S. A $$ (i, i))" . + finally have *: "(\i = 0..i\S. A $$ (i, i))" . show "(\i = 0.. carrier_mat n m" + assumes A: "A \ carrier_mat n m" and SNF_A: "Smith_normal_form_mat A" and k: "k \ min n m" shows "Gcd (minors A k) dvd (\i=0..i = 0..(i, j). A $$ (i, j))" proof (rule eq_matI, auto) have "I = {i. i < dim_row A \ i \ I}" unfolding I_def using A k by auto hence ck: "card {i. i < dim_row A \ i \ I} = k" unfolding I_def using card_atLeastLessThan by presburger have "I = {i. i < dim_col A \ i \ I}" unfolding I_def using A k by auto - hence ck2: "card {j. j < dim_col A \ j \ I} = k" + hence ck2: "card {j. j < dim_col A \ j \ I} = k" unfolding I_def using card_atLeastLessThan by presburger show dr: "dim_row (submatrix A I I) = k" using ck unfolding submatrix_def by auto show dc: "dim_col (submatrix A I I) = k" using ck2 unfolding submatrix_def by auto fix i j assume i: "i < k" and j: "j < k" have p1: "pick I i = i" proof - have "{0.. I. a < i}" using I_def i by auto hence i_eq: "i = card {a \ I. a < i}" by (metis card_atLeastLessThan diff_zero) have "pick I i = pick I (card {a \ I. a < i})" using i_eq by simp also have "... = i" by (rule pick_card_in_set, insert i I_def, simp) finally show ?thesis . qed have p2: "pick I j = j" proof - have "{0.. I. a < j}" using I_def j by auto hence j_eq: "j = card {a \ I. a < j}" by (metis card_atLeastLessThan diff_zero) have "pick I j = pick I (card {a \ I. a < j})" using j_eq by simp also have "... = j" by (rule pick_card_in_set, insert j I_def, simp) finally show ?thesis . qed have "submatrix A I I $$ (i, j) = A $$ (pick I i, pick I j)" proof (rule submatrix_index) show "i < card {i. i < dim_row A \ i \ I}" by (metis dim_submatrix(1) dr i) show "j < card {j. j < dim_col A \ j \ I}" by (metis dim_submatrix(2) dc j) qed also have "... = A $$ (i,j)" using p1 p2 by simp finally show "submatrix A I I $$ (i, j) = A $$ (i, j)" . qed hence "det (submatrix A I I) = det (mat k k (\(i, j). A $$ (i, j)))" by simp also have "... = prod_list (diag_mat (mat k k (\(i, j). A $$ (i, j))))" proof (rule det_upper_triangular) show "mat k k (\(i, j). A $$ (i, j)) \ carrier_mat k k" by auto - show "upper_triangular (Matrix.mat k k (\(i, j). A $$ (i, j)))" + show "upper_triangular (Matrix.mat k k (\(i, j). A $$ (i, j)))" using SNF_A A k unfolding Smith_normal_form_mat_def isDiagonal_mat_def by auto qed also have "... = (\i = 0.. {0.. {0..i = 0.. minors A k" unfolding minors_def by auto + ultimately show "(\i = 0.. minors A k" unfolding minors_def by auto qed lemma Gcd_minors_A_dvd_Gcd_minors_PAQ: fixes A::"'a::{semiring_Gcd,comm_ring_1} mat" - assumes A: "A \ carrier_mat m n" + assumes A: "A \ carrier_mat m n" and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" shows "Gcd (minors A k) dvd Gcd (minors (P*A*Q) k)" proof (rule Gcd_greatest) let ?B="(P * A * Q)" fix b assume "b \ minors ?B k" from this obtain I J where b: "b = det (submatrix ?B I J)" and I: "I \ {0.. {0.. {0.. carrier_mat m n" - and P: "P \ carrier_mat m m" + assumes A: "A \ carrier_mat m n" + and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" - and inv_P: "invertible_mat P" + and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" shows "Gcd (minors (P*A*Q) k) dvd Gcd (minors A k)" proof (rule Gcd_greatest) let ?B = "P * A * Q" fix b assume "b \ minors A k" from this obtain I J where b: "b = det (submatrix A I J)" and I: "I \ {0.. {0.. {0.. carrier_mat m m" using PP' P'P unfolding inverts_mat_def by (metis P carrier_matD(1) carrier_matD(2) carrier_matI index_mult_mat(3) index_one_mat(3)) have Q': "Q' \ carrier_mat n n" using QQ' Q'Q unfolding inverts_mat_def by (metis Q carrier_matD(1) carrier_matD(2) carrier_matI index_mult_mat(3) index_one_mat(3)) have rw: "P' *?B *Q' = A" proof - have f1: "P' * P = 1\<^sub>m m" by (metis (no_types) P' P'P carrier_matD(1) inverts_mat_def) have *: "P' * P * A = P' * (P * A)" by (meson A P P' assoc_mult_mat) have " P' * (P * A * Q) * Q' = P' * P * A * Q * Q'" by (smt A P P' Q assoc_mult_mat mult_carrier_mat) - also have "... = P' * P * (A * Q * Q')" + also have "... = P' * P * (A * Q * Q')" using A P P' Q Q' f1 * by auto also have "... = A * Q * Q'" using P'P A P' unfolding inverts_mat_def by auto also have "... = A" using QQ' A Q' Q unfolding inverts_mat_def by auto finally show ?thesis . qed have "Gcd (minors ?B k) dvd det (submatrix (P'*?B*Q') I J)" - by (rule Gcd_minors_dvd[OF _ P' _ Q' _ _ Ik Jk], insert P A Q I J, auto) + by (rule Gcd_minors_dvd[OF _ P' _ Q' _ _ Ik Jk], insert P A Q I J, auto) also have "... = det (submatrix A I J)" using rw by simp finally show "Gcd (minors ?B k) dvd b" using b by simp qed lemma Gcd_minors_dvd_diag_PAQ: - fixes P A Q::"'a::{semiring_Gcd,comm_ring_1} mat" - assumes A: "A \ carrier_mat m n" - and P: "P \ carrier_mat m m" + fixes P A Q::"'a::{semiring_Gcd,comm_ring_1} mat" + assumes A: "A \ carrier_mat m n" + and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" and SNF: "Smith_normal_form_mat (P*A*Q)" and k: "k\min m n" shows "Gcd (minors A k) dvd (\i=0..i=0.. carrier_mat m n" - and P: "P \ carrier_mat m m" + fixes P A Q::"'a::{semiring_Gcd,comm_ring_1} mat" + assumes A: "A \ carrier_mat m n" + and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" - and inv_P: "invertible_mat P" + and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" and SNF: "Smith_normal_form_mat (P*A*Q)" shows "(\i=0..i=0.. carrier_mat m n" and SNF: "Smith_normal_form_mat A" and prod_0: "(\j=0..Final theorem\ lemma Smith_normal_form_uniqueness_aux: - fixes P A Q::"'a::{idom,semiring_Gcd} mat" - assumes A: "A \ carrier_mat m n" + fixes P A Q::"'a::{idom,semiring_Gcd} mat" + assumes A: "A \ carrier_mat m n" (*PAQ = B with B in SNF and P,Q invertible matrices*) and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" - and inv_P: "invertible_mat P" + and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" and PAQ_B: "P*A*Q = B" and SNF: "Smith_normal_form_mat B" (*P'AQ' = B' with B' in SNF and P',Q' invertible matrices*) - and P': "P' \ carrier_mat m m" + and P': "P' \ carrier_mat m m" and Q': "Q' \ carrier_mat n n" - and inv_P': "invertible_mat P'" + and inv_P': "invertible_mat P'" and inv_Q': "invertible_mat Q'" and P'AQ'_B': "P'*A*Q' = B'" - and SNF_B': "Smith_normal_form_mat B'" - and k: "ki\k. B$$(i,i) dvd B'$$(i,i) \ B'$$(i,i) dvd B$$(i,i)" proof (rule allI, rule impI) fix i assume ik: "i \ k" - show " B $$ (i, i) dvd B' $$ (i, i) \ B' $$ (i, i) dvd B $$ (i, i)" + show " B $$ (i, i) dvd B' $$ (i, i) \ B' $$ (i, i) dvd B $$ (i, i)" proof - let ?\Bi = "(\i=0..B'i = "(\i=0..B'i dvd Gcd (minors A i)" - by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'], + have "?\B'i dvd Gcd (minors A i)" + by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'], insert P'AQ'_B' SNF_B' ik k, auto ) also have "... dvd ?\Bi" - by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q], + by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q], insert PAQ_B SNF ik k, auto) finally have B'_i_dvd_B_i: "?\B'i dvd ?\Bi" . - have "?\Bi dvd Gcd (minors A i)" - by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], + have "?\Bi dvd Gcd (minors A i)" + by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], insert PAQ_B SNF ik k, auto ) also have "... dvd ?\B'i" - by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], + by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], insert P'AQ'_B' SNF_B' ik k, auto) finally have B_i_dvd_B'_i: "?\Bi dvd ?\B'i" . let ?\B_Suc = "(\i=0..B'_Suc = "(\i=0..B'_Suc dvd Gcd (minors A (Suc i))" - by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'], + have "?\B'_Suc dvd Gcd (minors A (Suc i))" + by (unfold P'AQ'_B'[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P' Q' inv_P' inv_Q'], insert P'AQ'_B' SNF_B' ik k, auto ) also have "... dvd ?\B_Suc" - by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q], + by (unfold PAQ_B[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P Q], insert PAQ_B SNF ik k, auto) finally have 3: "?\B'_Suc dvd ?\B_Suc" . have "?\B_Suc dvd Gcd (minors A (Suc i))" - by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], + by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], insert PAQ_B SNF ik k, auto ) also have "... dvd ?\B'_Suc" - by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], + by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], insert P'AQ'_B' SNF_B' ik k, auto) - finally have 4: "?\B_Suc dvd ?\B'_Suc" . + finally have 4: "?\B_Suc dvd ?\B'_Suc" . show ?thesis proof (cases "?\B_Suc = 0") case True have True2: "?\B'_Suc = 0" using 4 True by fastforce - have "B$$(i,i) = 0" + have "B$$(i,i) = 0" by (rule Smith_prod_zero_imp_last_zero[OF _ SNF True], insert ik k PAQ_B P Q, auto) moreover have "B'$$(i,i) = 0" - by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2], + by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2], insert ik k P'AQ'_B' P' Q', auto) ultimately show ?thesis by auto next case False have "\u. u dvd 1 \ ?\B'i = u * ?\Bi" by (rule dvd_associated2[OF B'_i_dvd_B_i B_i_dvd_B'_i], insert False B'_i_dvd_B_i, force) - from this obtain u where eq1: "(\i=0..i=0..i=0..i=0..u. u dvd 1 \ ?\B_Suc = u * ?\B'_Suc" by (rule dvd_associated2[OF 4 3 False]) from this obtain w where eq2: "(\i=0..i=0..i=0..i=0..i=0..i=0..i=0..i=0..i=0..u. is_unit u \ B $$ (i, i) = u * B' $$ (i, i)" by auto thus ?thesis using dvd_associated2 by force qed qed qed lemma Smith_normal_form_uniqueness: - fixes P A Q::"'a::{idom,semiring_Gcd} mat" - assumes A: "A \ carrier_mat m n" + fixes P A Q::"'a::{idom,semiring_Gcd} mat" + assumes A: "A \ carrier_mat m n" (*PAQ = B with B in SNF and P,Q invertible matrices*) and P: "P \ carrier_mat m m" and Q: "Q \ carrier_mat n n" - and inv_P: "invertible_mat P" + and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q" and PAQ_B: "P*A*Q = B" and SNF: "Smith_normal_form_mat B" (*P'AQ' = B' with B' in SNF and P',Q' invertible matrices*) - and P': "P' \ carrier_mat m m" + and P': "P' \ carrier_mat m m" and Q': "Q' \ carrier_mat n n" - and inv_P': "invertible_mat P'" + and inv_P': "invertible_mat P'" and inv_Q': "invertible_mat Q'" and P'AQ'_B': "P'*A*Q' = B'" - and SNF_B': "Smith_normal_form_mat B'" + and SNF_B': "Smith_normal_form_mat B'" and i: "i < min m n" shows "\u. u dvd 1 \ B $$ (i,i) = u * B' $$ (i,i)" proof (cases "B $$ (i,i) = 0") case True let ?\B_Suc = "(\i=0..B'_Suc = "(\i=0..B_Suc dvd Gcd (minors A (Suc i))" - by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], + by (unfold PAQ_B[symmetric], rule diag_PAQ_dvd_Gcd_minors[OF A P Q inv_P inv_Q], insert PAQ_B SNF i, auto) also have "... dvd ?\B'_Suc" - by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], + by (unfold P'AQ'_B'[symmetric], rule Gcd_minors_dvd_diag_PAQ[OF A P' Q'], insert P'AQ'_B' SNF_B' i, auto) - finally have 4: "?\B_Suc dvd ?\B'_Suc" . + finally have 4: "?\B_Suc dvd ?\B'_Suc" . have prod0: "?\B_Suc=0" using True by auto have True2: "?\B'_Suc = 0" using 4 by (metis dvd_0_left_iff prod0) have "B'$$(i,i) = 0" - by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2], - insert i P'AQ'_B' P' Q', auto) + by (rule Smith_prod_zero_imp_last_zero[OF _ SNF_B' True2], + insert i P'AQ'_B' P' Q', auto) thus ?thesis using True by auto next case False - have "\a\i. B$$(a,a) dvd B'$$(a,a) \ B'$$(a,a) dvd B$$(a,a)" + have "\a\i. B$$(a,a) dvd B'$$(a,a) \ B'$$(a,a) dvd B$$(a,a)" by (rule Smith_normal_form_uniqueness_aux[OF assms]) hence "B$$(i,i) dvd B'$$(i,i) \ B'$$(i,i) dvd B$$(i,i)" using i by auto thus ?thesis using dvd_associated2 False by blast qed text \The final theorem, moved to HOL Analysis\ lemma Smith_normal_form_uniqueness_HOL_Analysis: fixes A::"'a::{idom,semiring_Gcd}^'m::mod_type^'n::mod_type" and P P'::"'a^'n::mod_type^'n::mod_type" and Q Q'::"'a^'m::mod_type^'m::mod_type" assumes - (*PAQ = B with B in SNF and P,Q invertible matrices*) - inv_P: "invertible P" + (*PAQ = B with B in SNF and P,Q invertible matrices*) + inv_P: "invertible P" and inv_Q: "invertible Q" and PAQ_B: "P**A**Q = B" and SNF: "Smith_normal_form B" (*P'AQ' = B' with B' in SNF and P',Q' invertible matrices*) - and inv_P': "invertible P'" + and inv_P': "invertible P'" and inv_Q': "invertible Q'" and P'AQ'_B': "P'**A**Q' = B'" - and SNF_B': "Smith_normal_form B'" + and SNF_B': "Smith_normal_form B'" and i: "i < min (nrows A) (ncols A)" - shows "\u. u dvd 1 \ B $h Mod_Type.from_nat i $h Mod_Type.from_nat i + shows "\u. u dvd 1 \ B $h Mod_Type.from_nat i $h Mod_Type.from_nat i = u * B' $h Mod_Type.from_nat i $h Mod_Type.from_nat i" proof - let ?P = "Mod_Type_Connect.from_hma\<^sub>m P" let ?A = "Mod_Type_Connect.from_hma\<^sub>m A" let ?Q = "Mod_Type_Connect.from_hma\<^sub>m Q" let ?B = "Mod_Type_Connect.from_hma\<^sub>m B" let ?P' = "Mod_Type_Connect.from_hma\<^sub>m P'" let ?Q' = "Mod_Type_Connect.from_hma\<^sub>m Q'" let ?B' = "Mod_Type_Connect.from_hma\<^sub>m B'" let ?i = "(Mod_Type.from_nat i)::'n" let ?i' = "(Mod_Type.from_nat i)::'m" have [transfer_rule]: "Mod_Type_Connect.HMA_M ?P P" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?A A" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?Q Q" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B B" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?P' P'" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?Q' Q'" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_M ?B' B'" by (simp add: Mod_Type_Connect.HMA_M_def) have [transfer_rule]: "Mod_Type_Connect.HMA_I i ?i" - by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE + by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE mod_type_class.to_nat_from_nat_id nrows_def) have [transfer_rule]: "Mod_Type_Connect.HMA_I i ?i'" - by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE + by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE mod_type_class.to_nat_from_nat_id ncols_def) have i2: "i < min CARD('m) CARD('n)" using i unfolding nrows_def ncols_def by auto - have "\u. u dvd 1 \ ?B $$(i,i) = u * ?B' $$ (i,i)" + have "\u. u dvd 1 \ ?B $$(i,i) = u * ?B' $$ (i,i)" proof (rule Smith_normal_form_uniqueness[of _ "CARD('n)" "CARD('m)"]) show "?P*?A*?Q=?B" using PAQ_B by (transfer', auto) show "Smith_normal_form_mat ?B" using SNF by (transfer', auto) show "?P'*?A*?Q'=?B'" using P'AQ'_B' by (transfer', auto) show "Smith_normal_form_mat ?B'" using SNF_B' by (transfer', auto) show "invertible_mat ?P" using inv_P by (transfer, auto) show "invertible_mat ?P'" using inv_P' by (transfer, auto) show "invertible_mat ?Q" using inv_Q by (transfer, auto) - show "invertible_mat ?Q'" using inv_Q' by (transfer, auto) + show "invertible_mat ?Q'" using inv_Q' by (transfer, auto) qed (insert i2, auto) hence "\u. u dvd 1 \ (index_hma B ?i ?i') = u * (index_hma B' ?i ?i')" by (transfer', rule) thus ?thesis unfolding index_hma_def by simp qed subsection \Uniqueness fixing a complete set of non-associates\ definition "Smith_normal_form_wrt A \ = ( - (\a b. Mod_Type.to_nat a = Mod_Type.to_nat b \ Mod_Type.to_nat a + 1 < nrows A + (\a b. Mod_Type.to_nat a = Mod_Type.to_nat b \ Mod_Type.to_nat a + 1 < nrows A \ Mod_Type.to_nat b + 1 < ncols A \ A $h a $h b dvd A $h (a+1) $h (b+1)) \ isDiagonal A \ Complete_set_non_associates \ - \ (\a b. Mod_Type.to_nat a = Mod_Type.to_nat b \ Mod_Type.to_nat a < min (nrows A) (ncols A) - \ Mod_Type.to_nat b < min (nrows A) (ncols A) \ A $h a $h b \ \) + \ (\a b. Mod_Type.to_nat a = Mod_Type.to_nat b \ Mod_Type.to_nat a < min (nrows A) (ncols A) + \ Mod_Type.to_nat b < min (nrows A) (ncols A) \ A $h a $h b \ \) )" lemma Smith_normal_form_wrt_uniqueness_HOL_Analysis: fixes A::"'a::{idom,semiring_Gcd}^'m::mod_type^'n::mod_type" and P P'::"'a^'n::mod_type^'n::mod_type" and Q Q'::"'a^'m::mod_type^'m::mod_type" assumes - (*PAQ = S with S in SNF and P,Q invertible matrices*) - P: "invertible P" + (*PAQ = S with S in SNF and P,Q invertible matrices*) + P: "invertible P" and Q: "invertible Q" and PAQ_S: "P**A**Q = S" and SNF: "Smith_normal_form_wrt S \" (*P'AQ' = S' with S' in SNF and P',Q' invertible matrices*) - and P': "invertible P'" + and P': "invertible P'" and Q': "invertible Q'" and P'AQ'_S': "P'**A**Q' = S'" - and SNF_S': "Smith_normal_form_wrt S' \" + and SNF_S': "Smith_normal_form_wrt S' \" shows "S = S'" proof - have "S $h i $h j = S' $h i $h j" for i j proof (cases "Mod_Type.to_nat i \ Mod_Type.to_nat j") case True then show ?thesis using SNF SNF_S' unfolding Smith_normal_form_wrt_def isDiagonal_def by auto next case False let ?i = "Mod_Type.to_nat i" let ?j = "Mod_Type.to_nat j" have complete_set: "Complete_set_non_associates \" using SNF_S' unfolding Smith_normal_form_wrt_def by simp have ij: "?i = ?j" using False by auto show ?thesis proof (rule ccontr) assume d: "S $h i $h j \ S' $h i $h j" have n: "normalize (S $h i $h j) \ normalize (S' $h i $h j)" proof (rule in_Ass_not_associated[OF complete_set _ _ d]) show "S $h i $h j \ \" using SNF unfolding Smith_normal_form_wrt_def by (metis False min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def) show "S' $h i $h j \ \" using SNF_S' unfolding Smith_normal_form_wrt_def - by (metis False min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def) - qed + by (metis False min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def) + qed have "\u. u dvd 1 \ S $h i $h j = u * S' $h i $h j" proof - - have "\u. u dvd 1 \ S $h Mod_Type.from_nat ?i $h Mod_Type.from_nat ?i + have "\u. u dvd 1 \ S $h Mod_Type.from_nat ?i $h Mod_Type.from_nat ?i = u * S' $h Mod_Type.from_nat ?i $h Mod_Type.from_nat ?i" proof (rule Smith_normal_form_uniqueness_HOL_Analysis[OF P Q PAQ_S _ P' Q' P'AQ'_S' _]) show "Smith_normal_form S" and "Smith_normal_form S'" using SNF SNF_S' Smith_normal_form_def Smith_normal_form_wrt_def by blast+ show "?i < min (nrows A) (ncols A)" by (metis ij min_less_iff_conj mod_type_class.to_nat_less_card ncols_def nrows_def) qed thus ?thesis using False by auto qed from this obtain u where "is_unit u" and "S $h i $h j = u * S' $h i $h j" by auto thus False using n by (simp add: normalize_1_iff normalize_mult) qed qed thus ?thesis by vector qed end \ No newline at end of file diff --git a/thys/Smith_Normal_Form/Smith_Certified.thy b/thys/Smith_Normal_Form/Smith_Certified.thy --- a/thys/Smith_Normal_Form/Smith_Certified.thy +++ b/thys/Smith_Normal_Form/Smith_Certified.thy @@ -1,125 +1,125 @@ (* Author: Jose Divasón - Email: jose.divason@unirioja.es + Email: jose.divason@unirioja.es *) section \A certified checker based on an external algorithm to compute Smith normal form\ theory Smith_Certified - imports + imports SNF_Algorithm_Euclidean_Domain begin -text\This (unspecified) function takes as input the matrix $A$ and returns five matrices -$(P,S,Q,P',Q')$, which must satisfy $S = PAQ$, $S$ is in Smith normal form, $P'$ and $Q'$ +text\This (unspecified) function takes as input the matrix $A$ and returns five matrices +$(P,S,Q,P',Q')$, which must satisfy $S = PAQ$, $S$ is in Smith normal form, $P'$ and $Q'$ are the inverse matrices of $P$ and $Q$ respectively\ text\The matrices are given in terms of lists for the sake of simplicity when connecting the function to external solvers, like Mathematica or Sage.\ -consts external_SNF :: - "int list list \ int list list \ int list list \ int list list \ int list list \ int list list" +consts external_SNF :: + "int list list \ int list list \ int list list \ int list list \ int list list \ int list list" text \We implement the checker by means of the following definition. The checker is implemented in the JNF representation of matrices to make use of the Strassen matrix multiplication algorithm. In case that the certification fails, then the verified Smith normal form algorithm is executed. Thus, we will always get a verified result.\ definition "checker_SNF A = ( let A' = mat_to_list A; m = dim_row A; n = dim_col A in case external_SNF A' of (P_ext,S_ext,Q_ext,P'_ext,Q'_ext) \ let P = mat_of_rows_list m P_ext; S = mat_of_rows_list m S_ext; Q = mat_of_rows_list m Q_ext; P' = mat_of_rows_list m P'_ext; Q' = mat_of_rows_list m Q'_ext in (if dim_row P = m \ dim_col P = m \ dim_row S = m \ dim_col S = n \ dim_row Q = n \ dim_col Q = n \ dim_row P' = m \ dim_col P' = m \ dim_row Q' = n \ dim_col Q' = n \ P * P' = 1\<^sub>m m \ Q * Q' = 1\<^sub>m n \ Smith_normal_form_mat S \ (S = P*A*Q) then (P,S,Q) else Code.abort (STR ''Certification failed'') (\ _. Smith_ED_mxn A)) )" theorem checker_SNF_soudness: assumes A: "A \ carrier_mat m n" and c: "checker_SNF A = (P,S,Q)" shows "is_SNF A (P,S,Q)" proof - - let ?ext = "external_SNF (mat_to_list A)" - obtain P_ext S_ext Q_ext P'_ext Q'_ext where ext: "?ext = (P_ext,S_ext,Q_ext,P'_ext,Q'_ext)" + let ?ext = "external_SNF (mat_to_list A)" + obtain P_ext S_ext Q_ext P'_ext Q'_ext where ext: "?ext = (P_ext,S_ext,Q_ext,P'_ext,Q'_ext)" by (cases "?ext", auto) let ?case_external = "let P = mat_of_rows_list m P_ext; S = mat_of_rows_list m S_ext; Q = mat_of_rows_list n Q_ext; P' = mat_of_rows_list m P'_ext; Q' = mat_of_rows_list n Q'_ext in (dim_row P = m \ dim_col P = m \ dim_row S = m \ dim_col S = n \ dim_row Q = n \ dim_col Q = n \ dim_row P' = m \ dim_col P' = m \ dim_row Q' = n \ dim_col Q' = n \ P * P' = 1\<^sub>m m \ Q * Q' = 1\<^sub>m n \ Smith_normal_form_mat S \ (S = P*A*Q))" - show ?thesis + show ?thesis proof (cases ?case_external) - case True + case True define P' where "P' = mat_of_rows_list m P'_ext" define Q' where "Q' = mat_of_rows_list m Q'_ext" - have S_PAQ: "S = P * A * Q " + have S_PAQ: "S = P * A * Q " and SNF_S: "Smith_normal_form_mat S" and PP'_1: "P * P' = 1\<^sub>m m" and QQ'_1: "Q * Q' = 1\<^sub>m n" and sm_P: "square_mat P" and sm_Q: "square_mat Q" - using ext True c A - unfolding checker_SNF_def Let_def mat_of_rows_list_def P'_def Q'_def + using ext True c A + unfolding checker_SNF_def Let_def mat_of_rows_list_def P'_def Q'_def by (auto split: if_splits) have inv_P: "invertible_mat P" - proof (unfold invertible_mat_def, rule conjI, rule sm_P, + proof (unfold invertible_mat_def, rule conjI, rule sm_P, unfold inverts_mat_def, rule exI[of _ P'], rule conjI) - show *: "P * P' = 1\<^sub>m (dim_row P)" - by (metis PP'_1 True index_mult_mat(2)) + show *: "P * P' = 1\<^sub>m (dim_row P)" + by (metis PP'_1 True index_mult_mat(2)) show "P' * P = 1\<^sub>m (dim_row P')" proof (rule mat_mult_left_right_inverse) show "P \ carrier_mat (dim_row P') (dim_row P')" by (metis * P'_def PP'_1 True carrier_mat_triv index_one_mat(2) sm_P square_mat.elims(2)) - show "P' \ carrier_mat (dim_row P') (dim_row P')" + show "P' \ carrier_mat (dim_row P') (dim_row P')" by (metis P'_def True carrier_mat_triv) show "P * P' = 1\<^sub>m (dim_row P')" by (metis P'_def PP'_1 True) qed qed have inv_Q: "invertible_mat Q" - proof (unfold invertible_mat_def, rule conjI, rule sm_Q, + proof (unfold invertible_mat_def, rule conjI, rule sm_Q, unfold inverts_mat_def, rule exI[of _ Q'], rule conjI) - show *: "Q * Q' = 1\<^sub>m (dim_row Q)" + show *: "Q * Q' = 1\<^sub>m (dim_row Q)" by (metis QQ'_1 True index_mult_mat(2)) show "Q' * Q = 1\<^sub>m (dim_row Q')" proof (rule mat_mult_left_right_inverse) - show 1: "Q \ carrier_mat (dim_row Q') (dim_row Q')" - by (metis Q'_def QQ'_1 True carrier_mat_triv dim_row_mat(1) index_mult_mat(2) + show 1: "Q \ carrier_mat (dim_row Q') (dim_row Q')" + by (metis Q'_def QQ'_1 True carrier_mat_triv dim_row_mat(1) index_mult_mat(2) mat_of_rows_list_def sm_Q square_mat.simps) thus "Q' \ carrier_mat (dim_row Q') (dim_row Q')" by (metis * carrier_matD(1) carrier_mat_triv index_mult_mat(3) index_one_mat(3)) show "Q * Q' = 1\<^sub>m (dim_row Q')" using * 1 by auto qed qed have "P \ carrier_mat m m" by (metis PP'_1 True carrier_matI index_mult_mat(2) sm_P square_mat.simps) moreover have "Q \ carrier_mat n n" by (metis QQ'_1 True carrier_matI index_mult_mat(2) sm_Q square_mat.simps) ultimately show ?thesis unfolding is_SNF_def using inv_P inv_Q SNF_S S_PAQ A by auto next case False - hence "checker_SNF A = Smith_ED_mxn A" - using ext False c A + hence "checker_SNF A = Smith_ED_mxn A" + using ext False c A unfolding checker_SNF_def Let_def Code.abort_def by (smt carrier_matD case_prod_conv dim_col_mat(1) mat_of_rows_list_def) - then show ?thesis using Smith_ED.is_SNF_Smith_mxn[OF A] c unfolding is_SNF_def + then show ?thesis using Smith_ED.is_SNF_Smith_mxn[OF A] c unfolding is_SNF_def by auto qed qed end