--- a/src/HOL/Matrix/Matrix.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Matrix/Matrix.thy Sat Jun 23 19:33:22 2007 +0200
@@ -59,17 +59,17 @@
show "A * B * C = A * (B * C)"
apply (simp add: times_matrix_def)
apply (rule mult_matrix_assoc)
- apply (simp_all add: associative_def ring_eq_simps)
+ apply (simp_all add: associative_def ring_simps)
done
show "(A + B) * C = A * C + B * C"
apply (simp add: times_matrix_def plus_matrix_def)
apply (rule l_distributive_matrix[simplified l_distributive_def, THEN spec, THEN spec, THEN spec])
- apply (simp_all add: associative_def commutative_def ring_eq_simps)
+ apply (simp_all add: associative_def commutative_def ring_simps)
done
show "A * (B + C) = A * B + A * C"
apply (simp add: times_matrix_def plus_matrix_def)
apply (rule r_distributive_matrix[simplified r_distributive_def, THEN spec, THEN spec, THEN spec])
- apply (simp_all add: associative_def commutative_def ring_eq_simps)
+ apply (simp_all add: associative_def commutative_def ring_simps)
done
show "abs A = sup A (-A)"
by (simp add: abs_matrix_def)
@@ -264,24 +264,24 @@
"scalar_mult a m == apply_matrix (op * a) m"
lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0"
- by (simp add: scalar_mult_def)
+by (simp add: scalar_mult_def)
lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
- by (simp add: scalar_mult_def apply_matrix_add ring_eq_simps)
+by (simp add: scalar_mult_def apply_matrix_add ring_simps)
lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)"
- by (simp add: scalar_mult_def)
+by (simp add: scalar_mult_def)
lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
- apply (subst Rep_matrix_inject[symmetric])
- apply (rule ext)+
- apply (auto)
- done
+apply (subst Rep_matrix_inject[symmetric])
+apply (rule ext)+
+apply (auto)
+done
lemma Rep_minus[simp]: "Rep_matrix (-(A::_::lordered_ab_group)) x y = - (Rep_matrix A x y)"
- by (simp add: minus_matrix_def)
+by (simp add: minus_matrix_def)
lemma Rep_abs[simp]: "Rep_matrix (abs (A::_::lordered_ring)) x y = abs (Rep_matrix A x y)"
- by (simp add: abs_lattice sup_matrix_def)
+by (simp add: abs_lattice sup_matrix_def)
end