imports Code_Cayley_Hamilton Examples_Gauss_Jordan_Abstract Echelon_Form_Inverse Field_as_Ring

(* Title: Examples_Echelon_Form_Abstract.thy Author: Jose Divasón <jose.divasonm at unirioja.es> Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> *) section‹Examples of execution over matrices represented as functions› theory Examples_Echelon_Form_Abstract imports Code_Cayley_Hamilton Gauss_Jordan.Examples_Gauss_Jordan_Abstract Echelon_Form_Inverse "HOL-Computational_Algebra.Field_as_Ring" begin text‹The definitions introduced in this file will be also used in the computations presented in file @{file ‹Examples_Echelon_Form_IArrays.thy›}. Some of these definitions are not even used in this file since they are quite time consuming.› definition test_real_6x4 :: "real^6^4" where "test_real_6x4 = list_of_list_to_matrix [[0,0,0,0,0,0], [0,1,0,0,0,0], [0,0,0,0,0,0], [0,0,0,0,8,2]]" value "matrix_to_list_of_list (minorM test_real_6x4 0 0)" value "cofactor (mat 1::rat^3^3) 0 0" value "vec_to_list (cofactorM_row (mat 1::int^3^3) 1)" value "matrix_to_list_of_list (cofactorM (mat 1::int^3^3))" definition test_rat_3x3 :: "rat^3^3" where "test_rat_3x3 = list_of_list_to_matrix [[3,5,1],[2,1,3],[1,2,1]]" value "matrix_to_list_of_list (matpow test_rat_3x3 5)" definition test_int_3x3 :: "int^3^3" where "test_int_3x3 = list_of_list_to_matrix [[3,2,8], [0,3,9], [8,7,9]]" value "det test_int_3x3" definition test_real_3x3 :: "real^3^3" where "test_real_3x3 = list_of_list_to_matrix [[3,5,1],[2,1,3],[1,2,1]]" value "charpoly test_real_3x3" text‹We check that the Cayley-Hamilton theorem holds for this particular case:› value "matrix_to_list_of_list (evalmat (charpoly test_real_3x3) test_real_3x3)" definition test_int_3x3_02 :: "int^3^3" where "test_int_3x3_02 = list_of_list_to_matrix [[3,5,1],[2,1,3],[1,2,1]]" value "matrix_to_list_of_list (adjugate test_int_3x3_02)" text‹The following integer matrix is not invertible, so the result is ‹None›› value "inverse_matrix test_int_3x3_02" definition test_int_3x3_03 :: "int^3^3" where "test_int_3x3_03 = list_of_list_to_matrix [[1,-2,4],[1,-1,1],[0,1,-2]]" value "matrix_to_list_of_list (the (inverse_matrix test_int_3x3_03))" text‹We check that the previous inverse has been correctly computed:› value "test_int_3x3_03 ** (the (inverse_matrix test_int_3x3_03)) = (mat 1::int^3^3)" definition test_int_8x8 :: "int^8^8" where "test_int_8x8 = list_of_list_to_matrix [[ 3, 2, 3, 6, 2, 8, 5, 6], [ 0, 5, 5, 2, 3, 9, 4, 7], [ 8, 7, 9, 1, 4,-2, 2, 0], [ 0, 1, 5, 6, 5, 1, 1, 4], [ 0, 3, 4, 5, 2,-4, 2, 1], [ 6, 8, 6, 2, 2,-3, 3, 5], [-2, 4,-2, 6, 7, 8, 0, 3], [ 7, 1, 3, 0,-9,-3, 4,-5]]" text‹SLOW; several minutes.› (*value "det test_int_8x8" value "matrix_to_list_of_list (echelon_form_of test_int_8x8 euclid_ext2)"*) text‹The following definitions will be used in file @{file ‹Examples_Echelon_Form_IArrays.thy›}. Using the abstract version of matrices would produce lengthy computations.› definition test_int_6x6 :: "int^6^6" where "test_int_6x6 = list_of_list_to_matrix [[ 3, 2, 3, 6, 2, 8], [ 0, 5, 5, 2, 3, 9], [ 8, 7, 9, 1, 4,-2], [ 0, 1, 5, 6, 5, 1], [ 0, 3, 4, 5, 2,-4], [ 6, 8, 6, 2, 2,-3]]" definition test_real_6x6 :: "real^6^6" where "test_real_6x6 = list_of_list_to_matrix [[ 3, 2, 3, 6, 2, 8], [ 0, 5, 5, 2, 3, 9], [ 8, 7, 9, 1, 4,-2], [ 0, 1, 5, 6, 5, 1], [ 0, 3, 4, 5, 2,-4], [ 6, 8, 6, 2, 2,-3]]" definition test_int_20x20 :: "int^20^20" where "test_int_20x20 = list_of_list_to_matrix [[3,2,3,6,2,8,5,9,8,7,5,4,7,8,9,8,7,4,5,2], [0,5,5,2,3,9,1,2,4,6,1,2,3,6,5,4,5,8,7,1], [8,7,9,1,4,-2,8,7,1,4,1,4,5,8,7,4,1,0,0,2], [0,1,5,6,5,1,3,5,4,9,3,2,1,4,5,6,9,8,7,4], [0,3,4,5,2,-4,0,2,1,0,0,0,1,2,4,5,1,1,2,0], [6,8,6,2,2,-3,2,4,7,9,1,2,3,6,5,4,1,2,8,7], [3,8,3,6,2,8,8,9,6,7,8,9,7,8,9,5,4,1,2,3,0], [0,8,5,2,8,9,1,2,4,6,4,6,5,8,7,9,8,7,4,5], [8,8,8,1,4,-2,8,7,1,4,5,5,5,6,4,5,1,2,3,6], [0,8,5,6,5,1,3,5,4,9::int,1,2,3,5,4,7,8,9,6,4], [3,2,3,6,2,8,5,9,8,7,5,4,7,3,9,8,7,4,5,2], [0,5,5,2,3,9,1,2,4,3,1,2,3,6,5,4,5,8,7,1], [1,7,9,1,4,-2,8,7,1,4,1,4,5,8,7,4,1,0,0,2], [1,1,5,6,5,1,3,5,4,9,3,4,5,6,9,8,7,4,5,4], [3,3,4,5,2,-4,0,2,1,0,0,3,1,2,4,5,1,1,2,0], [4,8,6,5,2,-3,2,4,2,9,1,2,3,2,5,4,1,2,8,7], [5,8,3,6,2,2,9,9,6,7,2,7,7,2,9,5,4,1,2,3,0], [2,8,5,2,8,9,5,2,4,6,4,6,5,2,7,1,8,7,4,5], [2,1,8,1,4,-2,8,3,1,4,5,5,5,6,4,5,1,2,3,6], [0,2,5,6,5,1,3,5,4,9::int,1,2,3,5,4,7,8,9,6,4]]" definition test_int_20x20_2 :: "int^20^20" where "test_int_20x20_2 = list_of_list_to_matrix [[58,18,18,41,68,62,6,21,19,78,34,22,108,63,71,38,43,52,37,24], [18,51,29,91,76,98,56,37,47,61,88,99,88,78,210,57,27,87,72,79], [49,19,81,107,43,34,69,28,101,39,21,910,27,53,15,38,5,34,47,23], [97,102,68,27,56,56,102,210,68,56,24,33,88,110,71,23,35,36,72,1], [63,11,39,16,32,81,16,98,94,26,53,23,11,51,98,51,81,57,610,85], [46,61,68,710,11,105,3,5,61,210,67,34,108,10,44,71,36,66,38,42], [39,75,106,42,36,92,110,42,89,105,11,108,22,61,65,101,410,1,1,31], [106,94,24,63,16,75,47,82,62,210,52,57,810,41,55,93,73,58,41,82], [55,49,102,9,8,41,12,110,109,310,95,51,103,71,92,85,910,410,17,21], [31,2,77,93,8,98,510,94,56,5,12,91,69,31,62,4,11,5,92,65], [22,29,103,34,64,11,9,610,1,19,35,24,21,49,31,43,81,102,14,11], [75,81,5,109,61,110,19,46,55,23,31,1,98,28,56,2,83,81,91,41], [4,510,58,41,38,106,99,103,31,84,110,63,17,105,210,61,95,103,63,51], [38,32,510,62,410,14,86,310,59,69,107,13,29,610,38,103,43,98,98,1], [101,11,3,101,99,810,10,3,510,8,35,62,45,49,34,86,63,66,71,9], [16,5,77,110,109,13,63,54,310,102,92,103,310,26,15,22,66,106,210,91], [13,810,66,51,91,84,19,25,110,41,51,87,27,79,18,69,99,95,11,46], [410,910,62,89,43,23,108,52,33,67,31,105,26,106,108,85,87,68,56,23], [310,68,21,91,107,85,94,28,101,34,109,27,63,84,25,106,65,81,7,310], [42,63,27,24,1010,11,107,69,910,810,31,15,97,3,56,77,51,108,31,26::int]]" end