src/HOL/Matrix/Matrix.thy
changeset 14662 d2c6a0f030ab
parent 14593 90c88e7ef62d
child 14691 e1eedc8cad37
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Apr 23 20:48:28 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Apr 23 20:49:26 2004 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4      License:    2004 Technische Universität München
     1.5  *)
     1.6  
     1.7 -theory Matrix=MatrixGeneral:
     1.8 +theory Matrix = MatrixGeneral:
     1.9  
    1.10  axclass almost_matrix_element < zero, plus, times
    1.11  matrix_add_assoc: "(a+b)+c = a + (b+c)"
    1.12 @@ -77,8 +77,8 @@
    1.13    have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
    1.14    note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
    1.15    {
    1.16 -    fix A::"('a::matrix_element) matrix" 
    1.17 -    fix B 
    1.18 +    fix A::"('a::matrix_element) matrix"
    1.19 +    fix B
    1.20      fix C
    1.21      have "(A + B) * C = A * C + B * C"
    1.22        apply (simp add: plus_matrix_def)
    1.23 @@ -86,15 +86,15 @@
    1.24        apply (rule l_distributive_matrix2)
    1.25        apply (simp_all add: associative_def commutative_def l_distributive_def)
    1.26        apply (auto)
    1.27 -      apply (simp_all add: matrix_add_assoc) 
    1.28 +      apply (simp_all add: matrix_add_assoc)
    1.29        apply (simp_all add: matrix_add_commute)
    1.30        by (simp_all add: matrix_left_distrib)
    1.31    }
    1.32    note left_distrib = this
    1.33    note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
    1.34    {
    1.35 -    fix A::"('a::matrix_element) matrix" 
    1.36 -    fix B 
    1.37 +    fix A::"('a::matrix_element) matrix"
    1.38 +    fix B
    1.39      fix C
    1.40      have "C * (A + B) = C * A + C * B"
    1.41        apply (simp add: plus_matrix_def)
    1.42 @@ -102,7 +102,7 @@
    1.43        apply (rule r_distributive_matrix2)
    1.44        apply (simp_all add: associative_def commutative_def r_distributive_def)
    1.45        apply (auto)
    1.46 -      apply (simp_all add: matrix_add_assoc) 
    1.47 +      apply (simp_all add: matrix_add_assoc)
    1.48        apply (simp_all add: matrix_add_commute)
    1.49        by (simp_all add: matrix_right_distrib)
    1.50    }
    1.51 @@ -175,12 +175,12 @@
    1.52  proof -
    1.53    assume p1:"a <= b"
    1.54    assume p2:"c <= d"
    1.55 -  have "a+c <= b+c" by (rule pordered_add_right_mono) 
    1.56 +  have "a+c <= b+c" by (rule pordered_add_right_mono)
    1.57    also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
    1.58    ultimately show "a+c <= b+d" by simp
    1.59  qed
    1.60  
    1.61 -instance matrix :: (pordered_matrix_element) pordered_matrix_element 
    1.62 +instance matrix :: (pordered_matrix_element) pordered_matrix_element
    1.63  apply (intro_classes)
    1.64  apply (simp_all add: plus_matrix_def times_matrix_def)
    1.65  apply (rule le_combine_matrix)
    1.66 @@ -246,9 +246,9 @@
    1.67  apply (simp_all)
    1.68  by (simp add: max_def nrows)
    1.69  
    1.70 -constdefs 
    1.71 +constdefs
    1.72    right_inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.73 -  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))" 
    1.74 +  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
    1.75    inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.76    "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
    1.77  
    1.78 @@ -256,28 +256,6 @@
    1.79  apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
    1.80  by (simp add: right_inverse_matrix_def)
    1.81  
    1.82 -(* to be continued \<dots> *)
    1.83 +text {* to be continued \dots *}
    1.84  
    1.85  end
    1.86 -
    1.87 -
    1.88 -
    1.89 -
    1.90 -
    1.91 -
    1.92 -
    1.93 -
    1.94 -
    1.95 -
    1.96 -  
    1.97 -  
    1.98 -
    1.99 -
   1.100 -
   1.101 -
   1.102 -
   1.103 -
   1.104 -
   1.105 -
   1.106 -
   1.107 -