# HG changeset patch
# User wenzelm
# Date 1267886069 -3600
# Node ID 0a9fb49a086d8014fcf6488632b1752bc1d1b81d
# Parent  07a8904f8fcd67ae0849df6e632944189007b18d
eliminated old-style prems;
tuned proofs;

diff -r 07a8904f8fcd -r 0a9fb49a086d src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Sat Mar 06 14:35:06 2010 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Sat Mar 06 15:34:29 2010 +0100
@@ -32,7 +32,7 @@
 
 lemma nrows:
   assumes hyp: "nrows A \<le> m"
-  shows "(Rep_matrix A m n) = 0" (is ?concl)
+  shows "(Rep_matrix A m n) = 0"
 proof cases
   assume "nonzero_positions(Rep_matrix A) = {}"
   then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
@@ -157,13 +157,13 @@
   ultimately show "False" using b by (simp)
 qed
 
-lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
+lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)"
 proof -
   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
-  show ?concl by (simp add: a ncols_le)
+  show ?thesis by (simp add: a ncols_le)
 qed
 
-lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"
 apply (auto)
 apply (subgoal_tac "ncols A <= m")
 apply (simp)
@@ -179,13 +179,13 @@
   finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
 qed
 
-lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
+lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)"
 proof -
   have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
-  show ?concl by (simp add: a nrows_le)
+  show ?thesis by (simp add: a nrows_le)
 qed
 
-lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"
 apply (auto)
 apply (subgoal_tac "nrows A <= m")
 apply (simp)
@@ -479,7 +479,7 @@
 
 lemma foldseq_significant_positions:
   assumes p: "! i. i <= N \<longrightarrow> S i = T i"
-  shows "foldseq f S N = foldseq f T N" (is ?concl)
+  shows "foldseq f S N = foldseq f T N"
 proof -
   have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
     apply (induct_tac m)
@@ -496,10 +496,12 @@
       have d:"!! s t. (\<forall>i\<le>n. s i = t i) \<Longrightarrow> foldseq f s n = foldseq f t n" by (simp add: a)
       show "f (t 0) (foldseq f (\<lambda>k. s (Suc k)) n) = f (t 0) (foldseq f (\<lambda>k. t (Suc k)) n)" by (rule c, simp add: d b)
     qed
-  with p show ?concl by simp
+  with p show ?thesis by simp
 qed
 
-lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")
+lemma foldseq_tail:
+  assumes "M <= N"
+  shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M"
 proof -
   have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
   have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
@@ -533,7 +535,7 @@
         apply (rule a)
         by (simp add: subc if_def)
     qed
-  then show "?p \<Longrightarrow> ?concl" by simp
+  then show ?thesis using assms by simp
 qed
 
 lemma foldseq_zerotail:
@@ -556,14 +558,13 @@
   assumes "! x. f x 0 = x"
   and "! i. n < i \<longrightarrow> s i = 0"
   and nm: "n <= m"
-  shows
-  "foldseq f s n = foldseq f s m" (is ?concl)
+  shows "foldseq f s n = foldseq f s m"
 proof -
-  have "f 0 0 = 0" by (simp add: prems)
+  have "f 0 0 = 0" by (simp add: assms)
   have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
   have c: "0 <= m" by simp
   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
-  show ?concl
+  show ?thesis
     apply (subst foldseq_tail[OF nm])
     apply (rule foldseq_significant_positions)
     apply (auto)
@@ -572,10 +573,11 @@
     apply (drule b[OF nm])
     apply (auto)
     apply (case_tac "k=0")
-    apply (simp add: prems)
+    apply (simp add: assms)
     apply (drule d)
     apply (auto)
-    by (simp add: prems foldseq_zero)
+    apply (simp add: assms foldseq_zero)
+    done
 qed
 
 lemma foldseq_zerostart:
@@ -623,11 +625,11 @@
 
 lemma foldseq_almostzero:
   assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
-  shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
+  shows "foldseq f s n = (if (j <= n) then (s j) else 0)"
 proof -
   from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
   from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
-  show ?concl
+  show ?thesis
     apply auto
     apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
     apply simp
@@ -639,7 +641,7 @@
 
 lemma foldseq_distr_unary:
   assumes "!! a b. g (f a b) = f (g a) (g b)"
-  shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
+  shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n"
 proof -
   have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
     apply (induct_tac n)
@@ -647,8 +649,8 @@
     apply (simp)
     apply (auto)
     apply (drule_tac x="% k. s (Suc k)" in spec)
-    by (simp add: prems)
-  then show ?concl by simp
+    by (simp add: assms)
+  then show ?thesis by simp
 qed
 
 definition mult_matrix_n :: "nat \<Rightarrow> (('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix" where
@@ -658,21 +660,24 @@
   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
 
 lemma mult_matrix_n:
-  assumes prems: "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
-  shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
+  assumes "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
+  shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B"
 proof -
-  show ?concl using prems
+  show ?thesis using assms
     apply (simp add: mult_matrix_def mult_matrix_n_def)
     apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
-    by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
+    apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms)
+    done
 qed
 
 lemma mult_matrix_nm:
-  assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
+  assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
   shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
 proof -
-  from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
-  also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
+  from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B"
+    by (simp add: mult_matrix_n)
+  also from assms have "\<dots> = mult_matrix_n m fmul fadd A B"
+    by (simp add: mult_matrix_n[THEN sym])
   finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
 qed
 
@@ -689,23 +694,23 @@
 lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
 
 lemma r_distributive_matrix:
- assumes prems:
+ assumes
   "r_distributive fmul fadd"
   "associative fadd"
   "commutative fadd"
   "fadd 0 0 = 0"
   "! a. fmul a 0 = 0"
   "! a. fmul 0 a = 0"
- shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
+ shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"
 proof -
-  from prems show ?concl
+  from assms show ?thesis
     apply (simp add: r_distributive_def mult_matrix_def, auto)
     proof -
       fix a::"'a matrix"
       fix u::"'b matrix"
       fix v::"'b matrix"
       let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
-      from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
+      from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
         combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"
         apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
         apply (simp add: max1 max2 combine_nrows combine_ncols)+
@@ -729,23 +734,23 @@
 qed
 
 lemma l_distributive_matrix:
- assumes prems:
+ assumes
   "l_distributive fmul fadd"
   "associative fadd"
   "commutative fadd"
   "fadd 0 0 = 0"
   "! a. fmul a 0 = 0"
   "! a. fmul 0 a = 0"
- shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
+ shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"
 proof -
-  from prems show ?concl
+  from assms show ?thesis
     apply (simp add: l_distributive_def mult_matrix_def, auto)
     proof -
       fix a::"'b matrix"
       fix u::"'a matrix"
       fix v::"'a matrix"
       let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
-      from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
+      from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
                combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"
         apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
         apply (simp add: max1 max2 combine_nrows combine_ncols)+
@@ -995,7 +1000,7 @@
 by (simp add: nrows)
 
 lemma mult_matrix_singleton_right[simp]:
-  assumes prems:
+  assumes
   "! x. fmul x 0 = 0"
   "! x. fmul 0 x = 0"
   "! x. fadd 0 x = x"
@@ -1004,11 +1009,11 @@
   apply (simp add: mult_matrix_def)
   apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
   apply (auto)
-  apply (simp add: prems)+
+  apply (simp add: assms)+
   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
   apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
   apply (subst foldseq_almostzero[of _ j])
-  apply (simp add: prems)+
+  apply (simp add: assms)+
   apply (auto)
   apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   done
@@ -1038,7 +1043,7 @@
   let ?S = "singleton_matrix I 0 e"
   let ?comp = "mult_matrix fmul fadd"
   have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
-  have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
+  have e: "(% x. fmul x e) 0 = 0" by (simp add: assms)
   have "~(?comp A ?S = ?comp B ?S)"
     apply (rule notI)
     apply (simp add: fprems eprops)
@@ -1058,12 +1063,12 @@
   assumes
   "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
   shows
-  "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
+  "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
 proof -
   have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
   have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
     apply (induct n)
-    apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
+    apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+
     apply (auto)
     by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
   show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
@@ -1083,7 +1088,7 @@
 shows
   "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
   apply (insert foldmatrix_transpose[of g f A m n])
-  by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
+  by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)
 
 lemma mult_n_nrows:
 assumes
@@ -1095,10 +1100,11 @@
 apply (simp add: mult_matrix_n_def)
 apply (subst RepAbs_matrix)
 apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows prems foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
 apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols prems foldseq_zero)
-by (simp add: nrows prems foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
+done
 
 lemma mult_n_ncols:
 assumes
@@ -1110,10 +1116,11 @@
 apply (simp add: mult_matrix_n_def)
 apply (subst RepAbs_matrix)
 apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows prems foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
 apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols prems foldseq_zero)
-by (simp add: ncols prems foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+done
 
 lemma mult_nrows:
 assumes
@@ -1121,7 +1128,7 @@
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
 shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
-by (simp add: mult_matrix_def mult_n_nrows prems)
+by (simp add: mult_matrix_def mult_n_nrows assms)
 
 lemma mult_ncols:
 assumes
@@ -1129,7 +1136,7 @@
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
 shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
-by (simp add: mult_matrix_def mult_n_ncols prems)
+by (simp add: mult_matrix_def mult_n_ncols assms)
 
 lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
   apply (auto simp add: nrows_le)
@@ -1144,7 +1151,7 @@
   done
 
 lemma mult_matrix_assoc:
-  assumes prems:
+  assumes
   "! a. fmul1 0 a = 0"
   "! a. fmul1 a 0 = 0"
   "! a. fmul2 0 a = 0"
@@ -1157,50 +1164,52 @@
   "! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
-  shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" (is ?concl)
+  shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)"
 proof -
   have comb_left:  "!! A B x y. A = B \<Longrightarrow> (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast
   have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (% k. fmul2 (s k) x) n"
-    by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
+    by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all)
   have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
-      by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
+    using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all)
   let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
-  show ?concl
+  show ?thesis
     apply (simp add: Rep_matrix_inject[THEN sym])
     apply (rule ext)+
     apply (simp add: mult_matrix_def)
     apply (simplesubst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
-    apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
+    apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
     apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
     apply (simp add: mult_matrix_n_def)
     apply (rule comb_left)
     apply ((rule ext)+, simp)
     apply (simplesubst RepAbs_matrix)
     apply (rule exI[of _ "nrows B"])
-    apply (simp add: nrows prems foldseq_zero)
+    apply (simp add: nrows assms foldseq_zero)
     apply (rule exI[of _ "ncols C"])
-    apply (simp add: prems ncols foldseq_zero)
+    apply (simp add: assms ncols foldseq_zero)
     apply (subst RepAbs_matrix)
     apply (rule exI[of _ "nrows A"])
-    apply (simp add: nrows prems foldseq_zero)
+    apply (simp add: nrows assms foldseq_zero)
     apply (rule exI[of _ "ncols B"])
-    apply (simp add: prems ncols foldseq_zero)
-    apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
+    apply (simp add: assms ncols foldseq_zero)
+    apply (simp add: fmul2fadd1fold fmul1fadd2fold assms)
     apply (subst foldseq_foldseq)
-    apply (simp add: prems)+
-    by (simp add: transpose_infmatrix)
+    apply (simp add: assms)+
+    apply (simp add: transpose_infmatrix)
+    done
 qed
 
 lemma
-  assumes prems:
+  assumes
   "! a. fmul1 0 a = 0"
   "! a. fmul1 a 0 = 0"
   "! a. fmul2 0 a = 0"
@@ -1217,10 +1226,11 @@
   "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
 apply (rule ext)+
 apply (simp add: comp_def )
-by (simp add: mult_matrix_assoc prems)
+apply (simp add: mult_matrix_assoc assms)
+done
 
 lemma mult_matrix_assoc_simple:
-  assumes prems:
+  assumes
   "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
   "fadd 0 0 = 0"
@@ -1228,14 +1238,16 @@
   "commutative fadd"
   "associative fmul"
   "distributive fmul fadd"
-  shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" (is ?concl)
+  shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)"
 proof -
   have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
-    by (simp! add: associative_def commutative_def)
-  then show ?concl
+    using assms by (simp add: associative_def commutative_def)
+  then show ?thesis
     apply (subst mult_matrix_assoc)
-    apply (simp_all!)
-    by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
+    using assms
+    apply simp_all
+    apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def)
+    done
 qed
 
 lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
@@ -1258,9 +1270,10 @@
   foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
 apply (simp add: mult_matrix_def mult_matrix_n_def)
 apply (subst RepAbs_matrix)
-apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
-apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
-by simp
+apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero)
+apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero)
+apply simp
+done
 
 lemma transpose_mult_matrix:
   assumes
@@ -1272,7 +1285,9 @@
   "transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
   apply (simp add: Rep_matrix_inject[THEN sym])
   apply (rule ext)+
-  by (simp! add: Rep_mult_matrix max_ac)
+  using assms
+  apply (simp add: Rep_mult_matrix max_ac)
+  done
 
 lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
 apply (simp add:  Rep_matrix_inject[THEN sym])
@@ -1318,7 +1333,7 @@
   "(a::('a::{ord, zero}) matrix) <= b"
   shows
   "apply_matrix f a <= apply_matrix f b"
-  by (simp! add: le_matrix_def)
+  using assms by (simp add: le_matrix_def)
 
 lemma le_combine_matrix:
   assumes
@@ -1328,7 +1343,7 @@
   "C <= D"
   shows
   "combine_matrix f A C <= combine_matrix f B D"
-by (simp! add: le_matrix_def)
+  using assms by (simp add: le_matrix_def)
 
 lemma le_left_combine_matrix:
   assumes
@@ -1337,7 +1352,7 @@
   "A <= B"
   shows
   "combine_matrix f C A <= combine_matrix f C B"
-  by (simp! add: le_matrix_def)
+  using assms by (simp add: le_matrix_def)
 
 lemma le_right_combine_matrix:
   assumes
@@ -1346,7 +1361,7 @@
   "A <= B"
   shows
   "combine_matrix f A C <= combine_matrix f B C"
-  by (simp! add: le_matrix_def)
+  using assms by (simp add: le_matrix_def)
 
 lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
   by (simp add: le_matrix_def, auto)
@@ -1358,8 +1373,9 @@
   shows
   "foldseq f s n <= foldseq f t n"
 proof -
-  have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!)
-  then show "foldseq f s n <= foldseq f t n" by (simp!)
+  have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n"
+    by (induct n) (simp_all add: assms)
+  then show "foldseq f s n <= foldseq f t n" using assms by simp
 qed
 
 lemma le_left_mult:
@@ -1373,11 +1389,13 @@
   "A <= B"
   shows
   "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
-  apply (simp! add: le_matrix_def Rep_mult_matrix)
+  using assms
+  apply (simp add: le_matrix_def Rep_mult_matrix)
   apply (auto)
   apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
   apply (rule le_foldseq)
-  by (auto)
+  apply (auto)
+  done
 
 lemma le_right_mult:
   assumes
@@ -1390,11 +1408,13 @@
   "A <= B"
   shows
   "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
-  apply (simp! add: le_matrix_def Rep_mult_matrix)
+  using assms
+  apply (simp add: le_matrix_def Rep_mult_matrix)
   apply (auto)
   apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
   apply (rule le_foldseq)
-  by (auto)
+  apply (auto)
+  done
 
 lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
 lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
@@ -1720,15 +1740,16 @@
 proof -
   have "Y = Y * one_matrix (nrows A)" 
     apply (subst one_matrix_mult_right)
-    apply (insert prems)
-    by (simp_all add: left_inverse_matrix_def)
+    using assms
+    apply (simp_all add: left_inverse_matrix_def)
+    done
   also have "\<dots> = Y * (A * X)" 
-    apply (insert prems)
+    apply (insert assms)
     apply (frule right_inverse_matrix_dim)
     by (simp add: right_inverse_matrix_def)
   also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
   also have "\<dots> = X" 
-    apply (insert prems)
+    apply (insert assms)
     apply (frule left_inverse_matrix_dim)
     apply (simp_all add:  left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
     done