merged

--- a/src/HOL/Matrix_LP/Matrix.thy	Fri Aug 23 23:16:53 2024 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy	Sat Aug 24 14:14:57 2024 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Matrix_LP/Matrix.thy
-    Author:     Steven Obua
+    Author:     Steven Obua; updated to Isar by LCP
 *)
 
 theory Matrix
@@ -69,43 +69,26 @@
 by ((rule ext)+, simp)
 
 lemma transpose_infmatrix: "transpose_infmatrix (\<lambda>j i. P j i) = (\<lambda>j i. P i j)"
-  apply (rule ext)+
-  by simp
+  by force
 
 lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
-apply (rule Abs_matrix_inverse)
-apply (simp add: matrix_def nonzero_positions_def image_def)
 proof -
   let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
+  let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
   let ?swap = "\<lambda>pos. (snd pos, fst pos)"
-  let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
-  have swap_image: "?swap`?A = ?B"
-    apply (simp add: image_def)
-    apply (rule set_eqI)
-    apply (simp)
-    proof
-      fix y
-      assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
-      thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
-        proof -
-          from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
-          then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
-        qed
-    next
-      fix y
-      assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
-      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
-        by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
-    qed
-  then have "finite (?swap`?A)"
-    proof -
-      have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
-      then have "finite ?B" by (simp add: nonzero_positions_def)
-      with swap_image show "finite (?swap`?A)" by (simp)
-    qed
-  moreover
-  have "inj_on ?swap ?A" by (simp add: inj_on_def)
-  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
+  have "finite ?A"
+  proof -
+    have swap_image: "?swap`?A = ?B"
+      by (force simp add: image_def)
+    then have "finite (?swap`?A)"
+      by (metis (full_types) finite_nonzero_positions nonzero_positions_def)
+    moreover
+    have "inj_on ?swap ?A" by (simp add: inj_on_def)
+    ultimately show "finite ?A"
+      using finite_imageD by blast
+  qed
+  then show ?thesis
+    by (simp add: Abs_matrix_inverse matrix_def nonzero_positions_def)
 qed
 
 lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b"
@@ -134,52 +117,38 @@
   by (metis nrows nrows_transpose transpose_matrix)
 
 lemma ncols_le: "(ncols A \<le> n) \<longleftrightarrow> (\<forall>j i. n \<le> i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
-apply (auto)
-apply (simp add: ncols)
-proof (simp add: ncols_def, auto)
-  let ?P = "nonzero_positions (Rep_matrix A)"
-  let ?p = "snd`?P"
-  have a:"finite ?p" by (simp add: finite_nonzero_positions)
-  let ?m = "Max ?p"
-  assume "~(Suc (?m) \<le> n)"
-  then have b:"n \<le> ?m" by (simp)
-  fix a b
-  assume "(a,b) \<in> ?P"
-  then have "?p \<noteq> {}" by (auto)
-  with a have "?m \<in>  ?p" by (simp)
-  moreover have "\<forall>x. (x \<in> ?p \<longrightarrow> (\<exists>y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
-  ultimately have "\<exists>y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
-  moreover assume ?st
-  ultimately show "False" using b by (simp)
+proof -
+  have "Rep_matrix A j i = 0"
+    if "ncols A \<le> n" "n \<le> i" for j i
+    by (meson that le_trans ncols)
+  moreover have "ncols A \<le> n"
+    if "\<forall>j i. n \<le> i \<longrightarrow> Rep_matrix A j i = 0"
+    unfolding ncols_def
+  proof (clarsimp split: if_split_asm)
+    assume \<section>: "nonzero_positions (Rep_matrix A) \<noteq> {}"
+    let ?P = "nonzero_positions (Rep_matrix A)"
+    let ?p = "snd`?P"
+    have a:"finite ?p" by (simp add: finite_nonzero_positions)
+    let ?m = "Max ?p"
+    show "Suc (Max (snd ` nonzero_positions (Rep_matrix A))) \<le> n"
+      using \<section> that  obtains_MAX [OF finite_nonzero_positions]
+      by (metis (mono_tags, lifting) mem_Collect_eq nonzero_positions_def not_less_eq_eq)
+  qed
+  ultimately show ?thesis
+    by auto
 qed
 
-lemma less_ncols: "(n < ncols A) = (\<exists>j i. n \<le> i & (Rep_matrix A j i) \<noteq> 0)"
-proof -
-  have a: "!! (a::nat) b. (a < b) = (~(b \<le> a))" by arith
-  show ?thesis by (simp add: a ncols_le)
-qed
+lemma less_ncols: "(n < ncols A) = (\<exists>j i. n \<le> i \<and> (Rep_matrix A j i) \<noteq> 0)"
+  by (meson linorder_not_le ncols_le)
 
 lemma le_ncols: "(n \<le> ncols A) = (\<forall> m. (\<forall> j i. m \<le> i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n \<le> m)"
-apply (auto)
-apply (subgoal_tac "ncols A \<le> m")
-apply (simp)
-apply (simp add: ncols_le)
-apply (drule_tac x="ncols A" in spec)
-by (simp add: ncols)
+  by (meson le_trans ncols ncols_le)
 
 lemma nrows_le: "(nrows A \<le> n) = (\<forall>j i. n \<le> j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
-proof -
-  have "(nrows A \<le> n) = (ncols (transpose_matrix A) \<le> n)" by (simp)
-  also have "\<dots> = (\<forall>j i. n \<le> i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
-  also have "\<dots> = (\<forall>j i. n \<le> i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
-  finally show "(nrows A \<le> n) = (\<forall>j i. n \<le> j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
-qed
+  by (metis ncols_le ncols_transpose transpose_matrix)
 
-lemma less_nrows: "(m < nrows A) = (\<exists>j i. m \<le> j & (Rep_matrix A j i) \<noteq> 0)"
-proof -
-  have a: "!! (a::nat) b. (a < b) = (~(b \<le> a))" by arith
-  show ?thesis by (simp add: a nrows_le)
-qed
+lemma less_nrows: "(m < nrows A) = (\<exists>j i. m \<le> j \<and> (Rep_matrix A j i) \<noteq> 0)"
+  by (meson linorder_not_le nrows_le)
 
 lemma le_nrows: "(n \<le> nrows A) = (\<forall> m. (\<forall> j i. m \<le> j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n \<le> m)"
   by (meson order.trans nrows nrows_le)
@@ -191,33 +160,31 @@
   by (meson leI ncols)
 
 lemma finite_natarray1: "finite {x. x < (n::nat)}"
-  by (induct n) auto
+  by simp
 
-lemma finite_natarray2: "finite {(x, y). x < (m::nat) & y < (n::nat)}"
+lemma finite_natarray2: "finite {(x, y). x < (m::nat) \<and> y < (n::nat)}"
   by simp
 
 lemma RepAbs_matrix:
-  assumes aem: "\<exists>m. \<forall>j i. m \<le> j \<longrightarrow> x j i = 0" (is ?em) and aen:"\<exists>n. \<forall>j i. (n \<le> i \<longrightarrow> x j i = 0)" (is ?en)
+  assumes "\<exists>m. \<forall>j i. m \<le> j \<longrightarrow> x j i = 0"  
+    and "\<exists>n. \<forall>j i. (n \<le> i \<longrightarrow> x j i = 0)" 
   shows "(Rep_matrix (Abs_matrix x)) = x"
-apply (rule Abs_matrix_inverse)
-apply (simp add: matrix_def nonzero_positions_def)
 proof -
-  from aem obtain m where a: "\<forall>j i. m \<le> j \<longrightarrow> x j i = 0" by (blast)
-  from aen obtain n where b: "\<forall>j i. n \<le> i \<longrightarrow> x j i = 0" by (blast)
-  let ?u = "{(i, j). x i j \<noteq> 0}"
-  let ?v = "{(i, j). i < m & j < n}"
-  have c: "!! (m::nat) a. ~(m \<le> a) \<Longrightarrow> a < m" by (arith)
-  from a b have "(?u \<inter> (-?v)) = {}"
-    apply (simp)
-    apply (rule set_eqI)
-    apply (simp)
-    apply auto
-    by (rule c, auto)+
-  then have d: "?u \<subseteq> ?v" by blast
-  moreover have "finite ?v" by (simp add: finite_natarray2)
-  moreover have "{pos. x (fst pos) (snd pos) \<noteq> 0} = ?u" by auto
-  ultimately show "finite {pos. x (fst pos) (snd pos) \<noteq> 0}"
-    by (metis (lifting) finite_subset)
+  have "finite {pos. x (fst pos) (snd pos) \<noteq> 0}"
+  proof -
+    from assms obtain m n where a: "\<forall>j i. m \<le> j \<longrightarrow> x j i = 0" 
+      and b: "\<forall>j i. n \<le> i \<longrightarrow> x j i = 0" by (blast)
+    let ?u = "{(i, j). x i j \<noteq> 0}"
+    let ?v = "{(i, j). i < m \<and> j < n}"
+    have c: "\<And>(m::nat) a. ~(m \<le> a) \<Longrightarrow> a < m" by (arith)
+    with a b have d: "?u \<subseteq> ?v" by blast
+    moreover have "finite ?v" by (simp add: finite_natarray2)
+    moreover have "{pos. x (fst pos) (snd pos) \<noteq> 0} = ?u" by auto
+    ultimately show "finite {pos. x (fst pos) (snd pos) \<noteq> 0}"
+      by (metis (lifting) finite_subset)
+  qed
+  then show ?thesis
+    by (simp add: Abs_matrix_inverse matrix_def nonzero_positions_def)
 qed
 
 definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where
@@ -277,10 +244,9 @@
 
 lemma combine_infmatrix_closed [simp]:
   "f 0 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))) = combine_infmatrix f (Rep_matrix A) (Rep_matrix B)"
-apply (rule Abs_matrix_inverse)
-apply (simp add: matrix_def)
-apply (rule finite_subset[of _ "(nonzero_positions (Rep_matrix A)) \<union> (nonzero_positions (Rep_matrix B))"])
-by (simp_all)
+  apply (rule Abs_matrix_inverse)
+  apply (simp add: matrix_def)
+  by (meson finite_Un finite_nonzero_positions_Rep finite_subset nonzero_positions_combine_infmatrix)
 
 text \<open>We need the next two lemmas only later, but it is analog to the above one, so we prove them now:\<close>
 lemma nonzero_positions_apply_infmatrix[simp]: "f 0 = 0 \<Longrightarrow> nonzero_positions (apply_infmatrix f A) \<subseteq> nonzero_positions A"
@@ -290,31 +256,25 @@
   "f 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (apply_infmatrix f (Rep_matrix A))) = apply_infmatrix f (Rep_matrix A)"
 apply (rule Abs_matrix_inverse)
 apply (simp add: matrix_def)
-apply (rule finite_subset[of _ "nonzero_positions (Rep_matrix A)"])
-by (simp_all)
+  by (meson finite_nonzero_positions_Rep finite_subset nonzero_positions_apply_infmatrix)
 
 lemma combine_infmatrix_assoc[simp]: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_infmatrix f)"
   by (simp add: associative_def combine_infmatrix_def)
 
-lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
-  by (auto)
-
 lemma combine_matrix_assoc: "f 0 0 = 0 \<Longrightarrow> associative f \<Longrightarrow> associative (combine_matrix f)"
-apply (simp(no_asm) add: associative_def combine_matrix_def, auto)
-apply (rule comb [of Abs_matrix Abs_matrix])
-by (auto, insert combine_infmatrix_assoc[of f], simp add: associative_def)
+  by (smt (verit) associative_def combine_infmatrix_assoc combine_infmatrix_closed combine_matrix_def)
 
 lemma Rep_apply_matrix[simp]: "f 0 = 0 \<Longrightarrow> Rep_matrix (apply_matrix f A) j i = f (Rep_matrix A j i)"
-by (simp add: apply_matrix_def)
+  by (simp add: apply_matrix_def)
 
 lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \<Longrightarrow> Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"
   by(simp add: combine_matrix_def)
 
 lemma combine_nrows_max: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) \<le> max (nrows A) (nrows B)"
-by (simp add: nrows_le)
+  by (simp add: nrows_le)
 
 lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) \<le> max (ncols A) (ncols B)"
-by (simp add: ncols_le)
+  by (simp add: ncols_le)
 
 lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A \<le> q \<Longrightarrow> nrows B \<le> q \<Longrightarrow> nrows(combine_matrix f A B) \<le> q"
   by (simp add: nrows_le)
@@ -329,7 +289,7 @@
   "zero_l_neutral f == \<forall>a. f 0 a = a"
 
 definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where
-  "zero_closed f == (\<forall>x. f x 0 = 0) & (\<forall>y. f 0 y = 0)"
+  "zero_closed f == (\<forall>x. f x 0 = 0) \<and> (\<forall>y. f 0 y = 0)"
 
 primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
 where
@@ -341,74 +301,61 @@
   "foldseq_transposed f s 0 = s 0"
 | "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
 
-lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
+lemma foldseq_assoc: 
+  assumes a:"associative f"
+  shows "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
 proof -
-  assume a:"associative f"
-  then have sublemma: "\<And>n. \<forall>N s. N \<le> n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
-  proof -
-    fix n
-    show "\<forall>N s. N \<le> n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
-    proof (induct n)
-      show "\<forall>N s. N \<le> 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
+  have "N \<le> n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" for N s n
+  proof (induct n arbitrary: N s)
+    case 0
+    then show ?case
+      by auto
+  next
+    case (Suc n)
+    show ?case
+    proof cases
+      assume "N \<le> n"
+      then show ?thesis
+        by (simp add: Suc.hyps)
     next
-      fix n
-      assume b: "\<forall>N s. N \<le> n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
-      have c:"\<And>N s. N \<le> n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
-      show "\<forall>N t. N \<le> Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
-      proof (auto)
-        fix N t
-        assume Nsuc: "N \<le> Suc n"
-        show "foldseq f t N = foldseq_transposed f t N"
-        proof cases
-          assume "N \<le> n"
-          then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
-        next
-          assume "~(N \<le> n)"
-          with Nsuc have Nsuceq: "N = Suc n" by simp
-          have neqz: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m & Suc m \<le> n" by arith
-          have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
-          show "foldseq f t N = foldseq_transposed f t N"
-            apply (simp add: Nsuceq)
-            apply (subst c)
-            apply (simp)
-            apply (case_tac "n = 0")
-            apply (simp)
-            apply (drule neqz)
-            apply (erule exE)
-            apply (simp)
-            apply (subst assocf)
-            proof -
-              fix m
-              assume "n = Suc m & Suc m \<le> n"
-              then have mless: "Suc m \<le> n" by arith
-              then have step1: "foldseq_transposed f (\<lambda>k. t (Suc k)) m = foldseq f (\<lambda>k. t (Suc k)) m" (is "?T1 = ?T2")
-                apply (subst c)
-                by simp+
-              have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
-              have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
-                apply (subst c)
-                by (simp add: mless)+
-              have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
-              from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
-            qed
-          qed
-        qed
+      assume "~(N \<le> n)"
+      then have Nsuceq: "N = Suc n"
+        using Suc.prems by linarith
+      have neqz: "n \<noteq> 0 \<Longrightarrow> \<exists>m. n = Suc m \<and> Suc m \<le> n" 
+        by arith
+      have assocf: "!! x y z. f x (f y z) = f (f x y) z"
+        by (metis a associative_def) 
+      have "f (f (s 0) (foldseq_transposed f (\<lambda>k. s (Suc k)) m)) (s (Suc (Suc m))) =
+                f (f (foldseq_transposed f s m) (s (Suc m))) (s (Suc (Suc m)))"
+        if "n = Suc m" for m
+      proof -
+        have \<section>: "foldseq_transposed f (\<lambda>k. s (Suc k)) m = foldseq f (\<lambda>k. s (Suc k)) m" (is "?T1 = ?T2")
+          by (simp add: Suc.hyps that)
+        have "f (s 0) ?T2 = foldseq f s (Suc m)" by simp
+        also have "\<dots> = foldseq_transposed f s (Suc m)" 
+          using Suc.hyps that by blast
+        also have "\<dots> = f (foldseq_transposed f s m) (s (Suc m))"  
+          by simp
+        finally show ?thesis
+          by (simp add: \<section>)
       qed
+      then show "foldseq f s N = foldseq_transposed f s N"
+        unfolding Nsuceq using assocf Suc.hyps neqz by force
     qed
-    show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
   qed
+  then show ?thesis
+    by blast
+qed
 
-lemma foldseq_distr: "\<lbrakk>associative f; commutative f\<rbrakk> \<Longrightarrow> foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"
+lemma foldseq_distr: 
+  assumes assoc: "associative f" and comm: "commutative f"
+  shows "foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"
 proof -
-  assume assoc: "associative f"
-  assume comm: "commutative f"
   from assoc have a:"!! x y z. f (f x y) z = f x (f y z)" by (simp add: associative_def)
   from comm have b: "!! x y. f x y = f y x" by (simp add: commutative_def)
   from assoc comm have c: "!! x y z. f x (f y z) = f y (f x z)" by (simp add: commutative_def associative_def)
-  have "\<And>n. (\<forall>u v. foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
-    apply (induct_tac n)
-    apply (simp+, auto)
-    by (simp add: a b c)
+  have "(\<forall>u v. foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))" for n
+    by (induct n) (simp_all add: assoc b c foldseq_assoc)
   then show "foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
 qed
 
@@ -431,76 +378,60 @@
 *)
 
 lemma foldseq_zero:
-assumes fz: "f 0 0 = 0" and sz: "\<forall>i. i \<le> n \<longrightarrow> s i = 0"
-shows "foldseq f s n = 0"
+  assumes fz: "f 0 0 = 0" and sz: "\<forall>i. i \<le> n \<longrightarrow> s i = 0"
+  shows "foldseq f s n = 0"
 proof -
-  have "\<And>n. \<forall>s. (\<forall>i. i \<le> n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
-    apply (induct_tac n)
-    apply (simp)
-    by (simp add: fz)
-  then show "foldseq f s n = 0" by (simp add: sz)
+  have "\<forall>s. (\<forall>i. i \<le> n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0" for n
+    by (induct n) (simp_all add: fz)
+  then show ?thesis 
+    by (simp add: sz)
 qed
 
 lemma foldseq_significant_positions:
   assumes p: "\<forall>i. i \<le> N \<longrightarrow> S i = T i"
   shows "foldseq f S N = foldseq f T N"
-proof -
-  have "\<And>m. \<forall>s t. (\<forall>i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
-    apply (induct_tac m)
-    apply (simp)
-    apply (simp)
-    apply (auto)
-    proof -
-      fix n
-      fix s::"nat\<Rightarrow>'a"
-      fix t::"nat\<Rightarrow>'a"
-      assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
-      assume b: "\<forall>i\<le>Suc n. s i = t i"
-      have c:"!! a b. a = b \<Longrightarrow> f (t 0) a = f (t 0) b" by blast
-      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 ?thesis by simp
+  using assms
+proof (induction N arbitrary: S T)
+  case 0
+  then show ?case by simp
+next
+  case (Suc N)
+  then show ?case
+    unfolding foldseq.simps by (metis not_less_eq_eq le0)
 qed
 
 lemma foldseq_tail:
   assumes "M \<le> N"
   shows "foldseq f S N = foldseq f (\<lambda>k. (if k < M then (S k) else (foldseq f (\<lambda>k. S(k+M)) (N-M)))) M"
-proof -
-  have suc: "\<And>a b. \<lbrakk>a \<le> Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a \<le> b" by arith
-  have a: "\<And>a b c . a = b \<Longrightarrow> f c a = f c b" by blast
-  have "\<And>n. \<forall>m s. m \<le> n \<longrightarrow> foldseq f s n = foldseq f (\<lambda>k. (if k < m then (s k) else (foldseq f (\<lambda>k. s(k+m)) (n-m)))) m"
-    apply (induct_tac n)
-    apply (simp)
-    apply (simp)
-    apply (auto)
-    apply (case_tac "m = Suc na")
-    apply (simp)
-    apply (rule a)
-    apply (rule foldseq_significant_positions)
-    apply (auto)
-    apply (drule suc, simp+)
-    proof -
-      fix na m s
-      assume suba:"\<forall>m\<le>na. \<forall>s. foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m"
-      assume subb:"m \<le> na"
-      from suba have subc:"!! m s. m \<le> na \<Longrightarrow>foldseq f s na = foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (na - m))m" by simp
-      have subd: "foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m =
-        foldseq f (\<lambda>k. s(Suc k)) na"
-        by (rule subc[of m "\<lambda>k. s(Suc k)", THEN sym], simp add: subb)
-      from subb have sube: "m \<noteq> 0 \<Longrightarrow> \<exists>mm. m = Suc mm & mm \<le> na" by arith
-      show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
-        foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
-        apply (simp add: subd)
-        apply (cases "m = 0")
-         apply simp
-        apply (drule sube)
-        apply auto
-        apply (rule a)
-        apply (simp add: subc cong del: if_weak_cong)
-        done
+  using assms
+proof (induction N arbitrary: M S)
+  case 0
+  then show ?case by auto
+next
+  case (Suc N)
+  show ?case
+  proof (cases "M = Suc N")
+    case True
+    then show ?thesis
+      by (auto intro!: arg_cong [of concl: "f (S 0)"] foldseq_significant_positions)
+  next
+    case False
+    then have "M\<le>N"
+      using Suc.prems by force
+    show ?thesis
+    proof (cases "M = 0")
+      case True
+      then show ?thesis
+        by auto
+    next
+      case False
+      then obtain M' where M': "M = Suc M'" "M' \<le> N"
+        by (metis Suc_leD \<open>M \<le> N\<close> nat.nchotomy)
+      then show ?thesis
+        apply (simp add:  Suc.IH [OF \<open>M'\<le>N\<close>])
+        using add_Suc_right diff_Suc_Suc by presburger
     qed
-  then show ?thesis using assms by simp
+  qed
 qed
 
 lemma foldseq_zerotail:
@@ -513,99 +444,73 @@
   assumes "\<forall>x. f x 0 = x"
   and "\<forall>i. n < i \<longrightarrow> s i = 0"
   and nm: "n \<le> m"
-  shows "foldseq f s n = foldseq f s m"
+shows "foldseq f s n = foldseq f s m"
 proof -
-  have "f 0 0 = 0" by (simp add: assms)
-  have b: "\<And>m n. n \<le> m \<Longrightarrow> m \<noteq> n \<Longrightarrow> \<exists>k. m-n = Suc k" by arith
-  have c: "0 \<le> m" by simp
-  have d: "\<And>k. k \<noteq> 0 \<Longrightarrow> \<exists>l. k = Suc l" by arith
-  show ?thesis
-    apply (subst foldseq_tail[OF nm])
-    apply (rule foldseq_significant_positions)
-    apply (auto)
-    apply (case_tac "m=n")
-    apply (simp+)
-    apply (drule b[OF nm])
-    apply (auto)
-    apply (case_tac "k=0")
-    apply (simp add: assms)
-    apply (drule d)
-    apply (auto)
-    apply (simp add: assms foldseq_zero)
-    done
+  have "s i = (if i < n then s i else foldseq f (\<lambda>k. s (k + n)) (m - n))"
+    if "i\<le>n" for i
+  proof (cases "m=n")
+    case True
+    then show ?thesis
+      using that by auto
+  next
+    case False
+    then obtain k where "m-n = Suc k"
+      by (metis Suc_diff_Suc le_neq_implies_less nm)
+    then show ?thesis
+      apply simp
+      by (simp add: assms(1,2) foldseq_zero nat_less_le that)
+  qed
+  then show ?thesis
+    unfolding foldseq_tail[OF nm]
+    by (auto intro: foldseq_significant_positions)
 qed
 
 lemma foldseq_zerostart:
-  "\<forall>x. f 0 (f 0 x) = f 0 x \<Longrightarrow> \<forall>i. i \<le> n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
-proof -
-  assume f00x: "\<forall>x. f 0 (f 0 x) = f 0 x"
-  have "\<forall>s. (\<forall>i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
-    apply (induct n)
-    apply (simp)
-    apply (rule allI, rule impI)
-    proof -
-      fix n
-      fix s
-      have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (\<lambda>k. s(Suc k)) (Suc n))" by simp
-      assume b: "\<forall>s. ((\<forall>i\<le>n. s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n)))"
-      from b have c:"!! s. (\<forall>i\<le>n. s i = 0) \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
-      assume d: "\<forall>i. i \<le> Suc n \<longrightarrow> s i = 0"
-      show "foldseq f s (Suc (Suc n)) = f 0 (s (Suc (Suc n)))"
-        apply (subst a)
-        apply (subst c)
-        by (simp add: d f00x)+
-    qed
-  then show "\<forall>i. i \<le> n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
+  assumes f00x: "\<forall>x. f 0 (f 0 x) = f 0 x" and 0: "\<forall>i. i \<le> n \<longrightarrow> s i = 0"
+  shows "foldseq f s (Suc n) = f 0 (s (Suc n))"
+  using 0
+proof (induction n arbitrary: s)
+  case 0
+  then show ?case by auto
+next
+  case (Suc n s)
+  then show ?case 
+    apply (simp add: le_Suc_eq)
+    by (smt (verit, ccfv_threshold) Suc.prems Suc_le_mono f00x foldseq_significant_positions le0)
 qed
 
 lemma foldseq_zerostart2:
-  "\<forall>x. f 0 x = x \<Longrightarrow> \<forall>i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
+  assumes x: "\<forall>x. f 0 x = x" and 0: "\<forall>i. i < n \<longrightarrow> s i = 0"
+  shows  "foldseq f s n = s n"
 proof -
-  assume a: "\<forall>i. i<n \<longrightarrow> s i = 0"
-  assume x: "\<forall>x. f 0 x = x"
-  from x have f00x: "\<forall>x. f 0 (f 0 x) = f 0 x" by blast
-  have b: "\<And>i l. i < Suc l = (i \<le> l)" by arith
-  have d: "\<And>k. k \<noteq> 0 \<Longrightarrow> \<exists>l. k = Suc l" by arith
   show "foldseq f s n = s n"
-  apply (case_tac "n=0")
-  apply (simp)
-  apply (insert a)
-  apply (drule d)
-  apply (auto)
-  apply (simp add: b)
-  apply (insert f00x)
-  apply (drule foldseq_zerostart)
-  by (simp add: x)+
+  proof (cases n)
+    case 0
+    then show ?thesis
+      by auto
+  next
+    case (Suc n')
+    then show ?thesis
+      by (metis "0" foldseq_zerostart le_imp_less_Suc x)
+  qed
 qed
 
 lemma foldseq_almostzero:
   assumes f0x: "\<forall>x. f 0 x = x" and fx0: "\<forall>x. f x 0 = x" and s0: "\<forall>i. i \<noteq> j \<longrightarrow> s i = 0"
   shows "foldseq f s n = (if (j \<le> n) then (s j) else 0)"
-proof -
-  from s0 have a: "\<forall>i. i < j \<longrightarrow> s i = 0" by simp
-  from s0 have b: "\<forall>i. j < i \<longrightarrow> s i = 0" by simp
-  show ?thesis
-    apply auto
-    apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
-    apply simp
-    apply (subst foldseq_zerostart2)
-    apply (simp add: f0x a)+
-    apply (subst foldseq_zero)
-    by (simp add: s0 f0x)+
-qed
+  by (smt (verit, ccfv_SIG) f0x foldseq_zerostart2 foldseq_zerotail2 fx0 le_refl nat_less_le s0)
 
 lemma foldseq_distr_unary:
-  assumes "!! a b. g (f a b) = f (g a) (g b)"
+  assumes "\<And>a b. g (f a b) = f (g a) (g b)"
   shows "g(foldseq f s n) = foldseq f (\<lambda>x. g(s x)) n"
-proof -
-  have "\<forall>s. g(foldseq f s n) = foldseq f (\<lambda>x. g(s x)) n"
-    apply (induct_tac n)
-    apply (simp)
-    apply (simp)
-    apply (auto)
-    apply (drule_tac x="\<lambda>k. s (Suc k)" in spec)
-    by (simp add: assms)
-  then show ?thesis by simp
+proof (induction n arbitrary: s)
+  case 0
+  then show ?case
+    by auto
+next
+  case (Suc n)
+  then show ?case
+    using assms by fastforce
 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
@@ -615,14 +520,15 @@
   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
 
 lemma mult_matrix_n:
-  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"
+  assumes "ncols A \<le>  n" "nrows B \<le> n" "fadd 0 0 = 0" "fmul 0 0 = 0"
+  shows "mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B"
 proof -
-  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)+)
-    apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms)
-    done
+  have "foldseq fadd (\<lambda>k. fmul (Rep_matrix A j k) (Rep_matrix B k i))
+                (max (ncols A) (nrows B)) =
+        foldseq fadd (\<lambda>k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n" for i j
+    using assms by (simp add: foldseq_zerotail nrows_le ncols_le)
+  then show ?thesis
+    by (simp add: mult_matrix_def mult_matrix_n_def)
 qed
 
 lemma mult_matrix_nm:
@@ -643,7 +549,7 @@
   "l_distributive fmul fadd == \<forall>a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
 
 definition distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where
-  "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd"
+  "distributive fmul fadd == l_distributive fmul fadd \<and> r_distributive fmul fadd"
 
 lemma max1: "!! a x y. (a::nat) \<le> x \<Longrightarrow> a \<le> max x y" by (arith)
 lemma max2: "!! b x y. (b::nat) \<le> y \<Longrightarrow> b \<le> max x y" by (arith)
@@ -675,7 +581,7 @@
         apply (simp add: max1 max2 combine_nrows combine_ncols)+
         apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
         apply (simp add: combine_matrix_def combine_infmatrix_def)
-        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
+        apply (intro ext arg_cong[of concl: "Abs_matrix"])
         apply (simplesubst RepAbs_matrix)
         apply (simp, auto)
         apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
@@ -715,7 +621,7 @@
         apply (simp add: max1 max2 combine_nrows combine_ncols)+
         apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
         apply (simp add: combine_matrix_def combine_infmatrix_def)
-        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
+        apply (intro ext arg_cong[of concl: "Abs_matrix"])
         apply (simplesubst RepAbs_matrix)
         apply (simp, auto)
         apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
@@ -738,21 +644,13 @@
 end
 
 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
-  apply (simp add: zero_matrix_def)
-  apply (subst RepAbs_matrix)
-  by (auto)
+  by (simp add: RepAbs_matrix zero_matrix_def)
 
 lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
-proof -
-  have a:"!! (x::nat). x \<le> 0 \<Longrightarrow> x = 0" by (arith)
-  show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
-qed
+  using nrows_le by force
 
 lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
-proof -
-  have a:"!! (x::nat). x \<le> 0 \<Longrightarrow> x = 0" by (arith)
-  show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
-qed
+  using ncols_le by fastforce
 
 lemma combine_matrix_zero_l_neutral: "zero_l_neutral f \<Longrightarrow> zero_l_neutral (combine_matrix f)"
   by (simp add: zero_l_neutral_def combine_matrix_def combine_infmatrix_def)
@@ -762,42 +660,34 @@
 
 lemma mult_matrix_zero_closed: "\<lbrakk>fadd 0 0 = 0; zero_closed fmul\<rbrakk> \<Longrightarrow> zero_closed (mult_matrix fmul fadd)"
   apply (simp add: zero_closed_def mult_matrix_def mult_matrix_n_def)
-  apply (auto)
-  by (subst foldseq_zero, (simp add: zero_matrix_def)+)+
+  by (simp add: foldseq_zero zero_matrix_def)
 
 lemma mult_matrix_n_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; \<forall>a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd A 0 = 0"
-  apply (simp add: mult_matrix_n_def)
-  apply (subst foldseq_zero)
-  by (simp_all add: zero_matrix_def)
+  by (simp add: RepAbs_matrix foldseq_zero matrix_eqI mult_matrix_n_def)
 
 lemma mult_matrix_n_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; \<forall>a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix_n n fmul fadd 0 A = 0"
-  apply (simp add: mult_matrix_n_def)
-  apply (subst foldseq_zero)
-  by (simp_all add: zero_matrix_def)
+  by (simp add: RepAbs_matrix foldseq_zero matrix_eqI mult_matrix_n_def)
 
 lemma mult_matrix_zero_left[simp]: "\<lbrakk>fadd 0 0 = 0; \<forall>a. fmul 0 a = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd 0 A = 0"
-by (simp add: mult_matrix_def)
+  by (simp add: mult_matrix_def)
 
 lemma mult_matrix_zero_right[simp]: "\<lbrakk>fadd 0 0 = 0; \<forall>a. fmul a 0 = 0\<rbrakk> \<Longrightarrow> mult_matrix fmul fadd A 0 = 0"
-by (simp add: mult_matrix_def)
+  by (simp add: mult_matrix_def)
 
 lemma apply_matrix_zero[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f 0 = 0"
-  apply (simp add: apply_matrix_def apply_infmatrix_def)
-  by (simp add: zero_matrix_def)
+  by (simp add: matrix_eqI)
 
 lemma combine_matrix_zero: "f 0 0 = 0 \<Longrightarrow> combine_matrix f 0 0 = 0"
-  apply (simp add: combine_matrix_def combine_infmatrix_def)
-  by (simp add: zero_matrix_def)
+  by (simp add: matrix_eqI)
 
 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
-  by (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix transpose_infmatrix)
+  by (simp add: matrix_eqI)
 
 lemma apply_zero_matrix_def[simp]: "apply_matrix (\<lambda>x. 0) A = 0"
-  apply (simp add: apply_matrix_def apply_infmatrix_def)
-  by (simp add: zero_matrix_def)
+  by (simp add: matrix_eqI)
 
 definition singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix" where
-  "singleton_matrix j i a == Abs_matrix(\<lambda>m n. if j = m & i = n then a else 0)"
+  "singleton_matrix j i a == Abs_matrix(\<lambda>m n. if j = m \<and> i = n then a else 0)"
 
 definition move_matrix :: "('a::zero) matrix \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a matrix" where
   "move_matrix A y x == Abs_matrix(\<lambda>j i. if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat ((int j)-y)) (nat ((int i)-x)))"
@@ -814,13 +704,9 @@
 definition row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
 
-lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m & i = n then e else 0)"
-apply (simp add: singleton_matrix_def)
-apply (auto)
-apply (subst RepAbs_matrix)
-apply (rule exI[of _ "Suc m"], simp)
-apply (rule exI[of _ "Suc n"], simp+)
-by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
+lemma Rep_singleton_matrix[simp]: "Rep_matrix (singleton_matrix j i e) m n = (if j = m \<and> i = n then e else 0)"
+  unfolding singleton_matrix_def
+  by (smt (verit, del_insts) RepAbs_matrix Suc_n_not_le_n)
 
 lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
   by (simp add: matrix_eqI)
@@ -829,47 +715,20 @@
   by (simp add: singleton_matrix_def zero_matrix_def)
 
 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
-proof-
-  have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
-from th show ?thesis 
-apply (auto)
-apply (rule le_antisym)
-apply (subst nrows_le)
-apply (simp add: singleton_matrix_def, auto)
-apply (subst RepAbs_matrix)
-apply auto
-apply (simp add: Suc_le_eq)
-apply (rule not_le_imp_less)
-apply (subst nrows_le)
-by simp
+proof -
+  have "e \<noteq> 0 \<Longrightarrow> Suc j \<le> nrows (singleton_matrix j i e)"
+    by (metis Rep_singleton_matrix not_less_eq_eq nrows)
+  then show ?thesis
+    by (simp add: le_antisym nrows_le)
 qed
 
 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
-proof-
-have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
-from th show ?thesis 
-apply (auto)
-apply (rule le_antisym)
-apply (subst ncols_le)
-apply (simp add: singleton_matrix_def, auto)
-apply (subst RepAbs_matrix)
-apply auto
-apply (simp add: Suc_le_eq)
-apply (rule not_le_imp_less)
-apply (subst ncols_le)
-by simp
-qed
+  by (simp add: Suc_leI le_antisym ncols_le ncols_notzero)
 
 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"
-apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
-apply (subst RepAbs_matrix)
-apply (rule exI[of _ "Suc j"], simp)
-apply (rule exI[of _ "Suc i"], simp)
-apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
-apply (subst RepAbs_matrix)
-apply (rule exI[of _ "Suc j"], simp)
-apply (rule exI[of _ "Suc i"], simp)
-by simp
+  apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
+  apply (intro ext arg_cong[of concl: "Abs_matrix"])
+  by (metis Rep_singleton_matrix singleton_matrix_def)
 
 lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
   by (simp add: matrix_eqI)
@@ -877,14 +736,13 @@
 lemma Rep_move_matrix[simp]:
   "Rep_matrix (move_matrix A y x) j i =
   (if (((int j)-y) < 0) | (((int i)-x) < 0) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
-apply (simp add: move_matrix_def)
-apply (auto)
+  apply (simp add: move_matrix_def)
 by (subst RepAbs_matrix,
   rule exI[of _ "(nrows A)+(nat \<bar>y\<bar>)"], auto, rule nrows, arith,
   rule exI[of _ "(ncols A)+(nat \<bar>x\<bar>)"], auto, rule ncols, arith)+
 
 lemma move_matrix_0_0[simp]: "move_matrix A 0 0 = A"
-by (simp add: move_matrix_def)
+  by (simp add: move_matrix_def)
 
 lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
   by (simp add: matrix_eqI)
@@ -895,28 +753,17 @@
 
 lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i =
   (if (j + int u < 0) | (i + int v < 0) then 0 else (singleton_matrix (nat (j + int u)) (nat (i + int v)) x))"
-  apply (intro matrix_eqI)
-  apply (split if_split)
-  apply (auto simp: split: if_split_asm)
-  done
+  by (auto intro!: matrix_eqI split: if_split_asm)
 
 lemma Rep_take_columns[simp]:
-  "Rep_matrix (take_columns A c) j i =
-  (if i < c then (Rep_matrix A j i) else 0)"
-apply (simp add: take_columns_def)
-apply (simplesubst RepAbs_matrix)
-apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
-apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
-done
+  "Rep_matrix (take_columns A c) j i = (if i < c then (Rep_matrix A j i) else 0)"
+  unfolding take_columns_def
+  by (smt (verit, best) RepAbs_matrix leD nrows)
 
 lemma Rep_take_rows[simp]:
-  "Rep_matrix (take_rows A r) j i =
-  (if j < r then (Rep_matrix A j i) else 0)"
-apply (simp add: take_rows_def)
-apply (simplesubst RepAbs_matrix)
-apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
-apply (rule exI[of _ "ncols A"], auto, simp add: ncols_le)
-done
+  "Rep_matrix (take_rows A r) j i = (if j < r then (Rep_matrix A j i) else 0)"
+  unfolding take_rows_def
+  by (smt (verit, best) RepAbs_matrix leD ncols)
 
 lemma Rep_column_of_matrix[simp]:
   "Rep_matrix (column_of_matrix A c) j i = (if i = 0 then (Rep_matrix A j c) else 0)"
@@ -933,22 +780,14 @@
   by (simp add: matrix_eqI nrows)
 
 lemma mult_matrix_singleton_right[simp]:
-  assumes
-  "\<forall>x. fmul x 0 = 0"
-  "\<forall>x. fmul 0 x = 0"
-  "\<forall>x. fadd 0 x = x"
-  "\<forall>x. fadd x 0 = x"
+  assumes "\<forall>x. fmul x 0 = 0" "\<forall>x. fmul 0 x = 0" "\<forall>x. fadd 0 x = x" "\<forall>x. fadd x 0 = x"
   shows "(mult_matrix fmul fadd A (singleton_matrix j i e)) = apply_matrix (\<lambda>x. fmul x e) (move_matrix (column_of_matrix A j) 0 (int i))"
-  apply (simp add: mult_matrix_def)
-  apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
-  apply (auto)
-  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: assms)+
-  apply (auto)
-  done
+  using assms
+  unfolding mult_matrix_def
+  apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"];
+         simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
+  apply (intro ext arg_cong[of concl: "Abs_matrix"])
+  by (simp add: max_def assms foldseq_almostzero[of _ j])
 
 lemma mult_matrix_ext:
   assumes
@@ -961,12 +800,10 @@
   "\<forall>a. fadd 0 a = a"
   and contraprems: "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
   shows "A = B"
-proof(rule contrapos_np[of "False"], simp)
-  assume a: "A \<noteq> B"
-  have b: "\<And>f g. (\<forall>x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
-  have "\<exists>j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
-    using Rep_matrix_inject a by blast
-  then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
+proof(rule ccontr)
+  assume "A \<noteq> B"
+  then obtain J I where ne: "(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)"
+    by (meson matrix_eqI)
   from eprem obtain e where eprops:"(\<forall>a b. a \<noteq> b \<longrightarrow> fmul a e \<noteq> fmul b e)" by blast
   let ?S = "singleton_matrix I 0 e"
   let ?comp = "mult_matrix fmul fadd"
@@ -975,8 +812,8 @@
   have "Rep_matrix (apply_matrix (\<lambda>x. fmul x e) (column_of_matrix A I)) \<noteq>
         Rep_matrix (apply_matrix (\<lambda>x. fmul x e) (column_of_matrix B I))"
     using fprems
-    by (metis Rep_apply_matrix Rep_column_of_matrix eprops c)
-  then have "~(?comp A ?S = ?comp B ?S)"
+    by (metis Rep_apply_matrix Rep_column_of_matrix eprops ne)
+  then have "?comp A ?S \<noteq> ?comp B ?S"
     by (simp add: fprems eprops Rep_matrix_inject)
   with contraprems show "False" by simp
 qed
@@ -988,95 +825,90 @@
   "foldmatrix_transposed f g A m n == foldseq g (\<lambda>j. foldseq_transposed f (A j) n) m"
 
 lemma foldmatrix_transpose:
-  assumes
-  "\<forall>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"
+  assumes "\<forall>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"
 proof -
   have forall:"\<And>P x. (\<forall>x. P x) \<Longrightarrow> P x" by auto
   have tworows:"\<forall>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 assms)+
-    apply (auto)
-    by (drule_tac x="(\<lambda>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"
-    apply (simp add: foldmatrix_def foldmatrix_transposed_def)
-    apply (induct m, simp)
-    apply (simp)
-    apply (insert tworows)
-    apply (drule_tac x="\<lambda>j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)
+  proof (induct n)
+    case 0
+    then show ?case 
+      by (simp add: foldmatrix_def foldmatrix_transposed_def)
+  next
+    case (Suc n)
+    then show ?case
+      apply (clarsimp simp: foldmatrix_def foldmatrix_transposed_def assms)
+      apply (rule arg_cong [of concl: "f _"])
+      by meson 
+  qed
+  have "foldseq_transposed g (\<lambda>j. foldseq f (A j) n) m =
+    foldseq f (\<lambda>j. foldseq_transposed g (transpose_infmatrix A j) m) n"
+  proof (induct m)
+    case 0
+    then show ?case by auto
+  next
+    case (Suc m)
+    then show ?case
+      using tworows
+      apply (drule_tac x="\<lambda>j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)
+      by (simp add: Suc foldmatrix_def foldmatrix_transposed_def)
+  qed
+  then show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
     by (simp add: foldmatrix_def foldmatrix_transposed_def)
 qed
 
 lemma foldseq_foldseq:
-assumes
-  "associative f"
-  "associative g"
-  "\<forall>a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
+assumes "associative f" "associative g" "\<forall>a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
 shows
   "foldseq g (\<lambda>j. foldseq f (A j) n) m = foldseq f (\<lambda>j. foldseq g ((transpose_infmatrix A) j) m) n"
-  apply (insert foldmatrix_transpose[of g f A m n])
+  using foldmatrix_transpose[of g f A m n]
   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)
 
 lemma mult_n_nrows:
-assumes
-"\<forall>a. fmul 0 a = 0"
-"\<forall>a. fmul a 0 = 0"
-"fadd 0 0 = 0"
-shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
-apply (subst nrows_le)
-apply (simp add: mult_matrix_n_def)
-apply (subst RepAbs_matrix)
-apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows assms foldseq_zero)
-apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols assms foldseq_zero)
-apply (simp add: nrows assms foldseq_zero)
-done
+  assumes "\<forall>a. fmul 0 a = 0" "\<forall>a. fmul a 0 = 0" "fadd 0 0 = 0"
+  shows "nrows (mult_matrix_n n fmul fadd A B) \<le> nrows A"
+  unfolding nrows_le mult_matrix_n_def
+  apply (subst RepAbs_matrix)
+    apply (rule_tac x="nrows A" in exI)
+    apply (simp add: nrows assms foldseq_zero)
+   apply (rule_tac x="ncols B" in exI)
+   apply (simp add: ncols assms foldseq_zero)
+  apply (simp add: nrows assms foldseq_zero)
+  done
 
 lemma mult_n_ncols:
-assumes
-"\<forall>a. fmul 0 a = 0"
-"\<forall>a. fmul a 0 = 0"
-"fadd 0 0 = 0"
-shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
-apply (subst ncols_le)
-apply (simp add: mult_matrix_n_def)
-apply (subst RepAbs_matrix)
-apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows assms foldseq_zero)
-apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols assms foldseq_zero)
-apply (simp add: ncols assms foldseq_zero)
-done
+  assumes "\<forall>a. fmul 0 a = 0" "\<forall>a. fmul a 0 = 0" "fadd 0 0 = 0"
+  shows "ncols (mult_matrix_n n fmul fadd A B) \<le> ncols B"
+  unfolding ncols_le mult_matrix_n_def
+  apply (subst RepAbs_matrix)
+    apply (rule_tac x="nrows A" in exI)
+    apply (simp add: nrows assms foldseq_zero)
+   apply (rule_tac x="ncols B" in exI)
+   apply (simp add: ncols assms foldseq_zero)
+  apply (simp add: ncols assms foldseq_zero)
+  done
 
 lemma mult_nrows:
-assumes
-"\<forall>a. fmul 0 a = 0"
-"\<forall>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 assms)
+  assumes
+    "\<forall>a. fmul 0 a = 0"
+    "\<forall>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 assms)
 
 lemma mult_ncols:
-assumes
-"\<forall>a. fmul 0 a = 0"
-"\<forall>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 assms)
+  assumes
+    "\<forall>a. fmul 0 a = 0"
+    "\<forall>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 assms)
 
 lemma nrows_move_matrix_le: "nrows (move_matrix A j i) \<le> nat((int (nrows A)) + j)"
-  apply (auto simp: nrows_le)
-  apply (rule nrows)
-  apply (arith)
-  done
+  by (smt (verit) Rep_move_matrix int_nat_eq nrows nrows_le of_nat_le_iff)
 
 lemma ncols_move_matrix_le: "ncols (move_matrix A j i) \<le> nat((int (ncols A)) + i)"
-  apply (auto simp: ncols_le)
-  apply (rule ncols)
-  apply (arith)
-  done
+  by (metis nrows_move_matrix_le nrows_transpose transpose_move_matrix)
 
 lemma mult_matrix_assoc:
   assumes
@@ -1104,78 +936,47 @@
     apply (intro matrix_eqI)
     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 assms)+
+          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 (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 assms)+
+          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 assms)+
+          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 assms)+
+          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 assms)+
+          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 assms foldseq_zero)
-    apply (rule exI[of _ "ncols C"])
-    apply (simp add: assms ncols foldseq_zero)
+      apply (rule exI[of _ "nrows B"])
+      apply (simp add: nrows assms foldseq_zero)
+     apply (rule exI[of _ "ncols C"])
+     apply (simp add: assms ncols foldseq_zero)
     apply (subst RepAbs_matrix)
-    apply (rule exI[of _ "nrows A"])
-    apply (simp add: nrows assms foldseq_zero)
-    apply (rule exI[of _ "ncols B"])
-    apply (simp add: assms ncols foldseq_zero)
+      apply (rule exI[of _ "nrows A"])
+      apply (simp add: nrows assms foldseq_zero)
+     apply (rule exI[of _ "ncols B"])
+     apply (simp add: assms ncols foldseq_zero)
     apply (simp add: fmul2fadd1fold fmul1fadd2fold assms)
     apply (subst foldseq_foldseq)
-    apply (simp add: assms)+
+       apply (simp add: assms)+
     apply (simp add: transpose_infmatrix)
     done
 qed
 
-lemma
-  assumes
-  "\<forall>a. fmul1 0 a = 0"
-  "\<forall>a. fmul1 a 0 = 0"
-  "\<forall>a. fmul2 0 a = 0"
-  "\<forall>a. fmul2 a 0 = 0"
-  "fadd1 0 0 = 0"
-  "fadd2 0 0 = 0"
-  "\<forall>a b c d. fadd2 (fadd1 a b) (fadd1 c d) = fadd1 (fadd2 a c) (fadd2 b d)"
-  "associative fadd1"
-  "associative fadd2"
-  "\<forall>a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
-  "\<forall>a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
-  "\<forall>a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
-  shows
-  "(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 )
-apply (simp add: mult_matrix_assoc assms)
-done
-
 lemma mult_matrix_assoc_simple:
   assumes
   "\<forall>a. fmul 0 a = 0"
   "\<forall>a. fmul a 0 = 0"
-  "fadd 0 0 = 0"
   "associative fadd"
   "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)"
-proof -
-  have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
-    using assms by (simp add: associative_def commutative_def)
-  then show ?thesis
-    apply (subst mult_matrix_assoc)
-    using assms
-    apply simp_all
-    apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def)
-    done
-qed
+  by (smt (verit) assms associative_def commutative_def distributive_def l_distributive_def mult_matrix_assoc r_distributive_def)
 
 lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
   by (simp add: matrix_eqI)
@@ -1184,19 +985,17 @@
   by (simp add: matrix_eqI)
 
 lemma Rep_mult_matrix:
-  assumes
-  "\<forall>a. fmul 0 a = 0"
-  "\<forall>a. fmul a 0 = 0"
-  "fadd 0 0 = 0"
+  assumes "\<forall>a. fmul 0 a = 0" "\<forall>a. fmul a 0 = 0" "fadd 0 0 = 0"
   shows
-  "Rep_matrix(mult_matrix fmul fadd A B) j i =
+    "Rep_matrix(mult_matrix fmul fadd A B) j i =
   foldseq fadd (\<lambda>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"], insert assms, simp add: nrows foldseq_zero)
-apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero)
-apply simp
-done
+  using assms
+  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)
+  apply simp
+  done
 
 lemma transpose_mult_matrix:
   assumes
@@ -1252,7 +1051,7 @@
 lemma le_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "\<forall>a b c d. a \<le> b & c \<le> d \<longrightarrow> f a c \<le> f b d"
+  "\<forall>a b c d. a \<le> b \<and> c \<le> d \<longrightarrow> f a c \<le> f b d"
   "A \<le> B"
   "C \<le> D"
   shows "combine_matrix f A C \<le> combine_matrix f B D"
@@ -1263,8 +1062,7 @@
   "f 0 0 = 0"
   "\<forall>a b c. a \<le> b \<longrightarrow> f c a \<le> f c b"
   "A \<le> B"
-  shows
-  "combine_matrix f C A \<le> combine_matrix f C B"
+  shows "combine_matrix f C A \<le> combine_matrix f C B"
   using assms by (simp add: le_matrix_def)
 
 lemma le_right_combine_matrix:
@@ -1272,8 +1070,7 @@
   "f 0 0 = 0"
   "\<forall>a b c. a \<le> b \<longrightarrow> f a c \<le> f b c"
   "A \<le> B"
-  shows
-  "combine_matrix f A C \<le> combine_matrix f B C"
+  shows "combine_matrix f A C \<le> combine_matrix f B C"
   using assms by (simp add: le_matrix_def)
 
 lemma le_transpose_matrix: "(A \<le> B) = (transpose_matrix A \<le> transpose_matrix B)"
@@ -1281,10 +1078,9 @@
 
 lemma le_foldseq:
   assumes
-  "\<forall>a b c d . a \<le> b & c \<le> d \<longrightarrow> f a c \<le> f b d"
+  "\<forall>a b c d . a \<le> b \<and> c \<le> d \<longrightarrow> f a c \<le> f b d"
   "\<forall>i. i \<le> n \<longrightarrow> s i \<le> t i"
-  shows
-  "foldseq f s n \<le> foldseq f t n"
+  shows "foldseq f s n \<le> foldseq f t n"
 proof -
   have "\<forall>s t. (\<forall>i. i<=n \<longrightarrow> s i \<le> t i) \<longrightarrow> foldseq f s n \<le> foldseq f t n"
     by (induct n) (simp_all add: assms)
@@ -1293,18 +1089,16 @@
 
 lemma le_left_mult:
   assumes
-  "\<forall>a b c d. a \<le> b & c \<le> d \<longrightarrow> fadd a c \<le> fadd b d"
-  "\<forall>c a b.   0 \<le> c & a \<le> b \<longrightarrow> fmul c a \<le> fmul c b"
+  "\<forall>a b c d. a \<le> b \<and> c \<le> d \<longrightarrow> fadd a c \<le> fadd b d"
+  "\<forall>c a b.   0 \<le> c \<and> a \<le> b \<longrightarrow> fmul c a \<le> fmul c b"
   "\<forall>a. fmul 0 a = 0"
   "\<forall>a. fmul a 0 = 0"
   "fadd 0 0 = 0"
   "0 \<le> C"
   "A \<le> B"
-  shows
-  "mult_matrix fmul fadd C A \<le> mult_matrix fmul fadd C B"
+  shows "mult_matrix fmul fadd C A \<le> mult_matrix fmul fadd C B"
   using assms
-  apply (simp add: le_matrix_def Rep_mult_matrix)
-  apply (auto)
+  apply (auto simp: le_matrix_def Rep_mult_matrix)
   apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
   apply (rule le_foldseq)
   apply (auto)
@@ -1312,62 +1106,70 @@
 
 lemma le_right_mult:
   assumes
-  "\<forall>a b c d. a \<le> b & c \<le> d \<longrightarrow> fadd a c \<le> fadd b d"
-  "\<forall>c a b. 0 \<le> c & a \<le> b \<longrightarrow> fmul a c \<le> fmul b c"
+  "\<forall>a b c d. a \<le> b \<and> c \<le> d \<longrightarrow> fadd a c \<le> fadd b d"
+  "\<forall>c a b. 0 \<le> c \<and> a \<le> b \<longrightarrow> fmul a c \<le> fmul b c"
   "\<forall>a. fmul 0 a = 0"
   "\<forall>a. fmul a 0 = 0"
   "fadd 0 0 = 0"
   "0 \<le> C"
   "A \<le> B"
-  shows
-  "mult_matrix fmul fadd A C \<le> mult_matrix fmul fadd B C"
+  shows "mult_matrix fmul fadd A C \<le> mult_matrix fmul fadd B C"
   using assms
-  apply (simp add: le_matrix_def Rep_mult_matrix)
-  apply (auto)
+  apply (auto simp: le_matrix_def Rep_mult_matrix)
   apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
   apply (rule le_foldseq)
   apply (auto)
   done
 
 lemma spec2: "\<forall>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
 
 lemma singleton_matrix_le[simp]: "(singleton_matrix j i a \<le> singleton_matrix j i b) = (a \<le> (b::_::order))"
   by (auto simp: le_matrix_def)
 
 lemma singleton_le_zero[simp]: "(singleton_matrix j i x \<le> 0) = (x \<le> (0::'a::{order,zero}))"
-  apply (auto)
-  apply (simp add: le_matrix_def)
-  apply (drule_tac j=j and i=i in spec2)
-  apply (simp)
-  apply (simp add: le_matrix_def)
-  done
+  by (metis singleton_matrix_le singleton_matrix_zero)
 
 lemma singleton_ge_zero[simp]: "(0 \<le> singleton_matrix j i x) = ((0::'a::{order,zero}) \<le> x)"
-  apply (auto)
-  apply (simp add: le_matrix_def)
-  apply (drule_tac j=j and i=i in spec2)
-  apply (simp)
-  apply (simp add: le_matrix_def)
-  done
+  by (metis singleton_matrix_le singleton_matrix_zero)
+
+lemma move_matrix_le_zero[simp]: 
+  fixes A:: "'a::{order,zero} matrix"
+  assumes "0 \<le> j" "0 \<le> i"
+  shows "(move_matrix A j i \<le> 0) = (A \<le> 0)"
+proof -
+  have "Rep_matrix A j' i' \<le> 0"
+    if "\<forall>n m. \<not> int n < j \<and> \<not> int m < i \<longrightarrow> Rep_matrix A (nat (int n - j)) (nat (int m - i)) \<le> 0"
+    for j' i'
+    using that[rule_format, of "j' + nat j" "i' + nat i"] by (simp add: assms)
+  then show ?thesis
+    by (auto simp: le_matrix_def)
+qed
 
-lemma move_matrix_le_zero[simp]: "0 \<le> j \<Longrightarrow> 0 \<le> i \<Longrightarrow> (move_matrix A j i \<le> 0) = (A \<le> (0::('a::{order,zero}) matrix))"
-  apply (auto simp: le_matrix_def)
-  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
-  apply (auto)
-  done
+lemma move_matrix_zero_le[simp]:
+  fixes A:: "'a::{order,zero} matrix"
+  assumes "0 \<le> j" "0 \<le> i"
+  shows  "(0 \<le> move_matrix A j i) = (0 \<le> A)"
+proof -
+  have "0 \<le> Rep_matrix A j' i'"
+    if "\<forall>n m. \<not> int n < j \<and> \<not> int m < i \<longrightarrow> 0 \<le> Rep_matrix A (nat (int n - j)) (nat (int m - i))"
+    for j' i'
+    using that[rule_format, of "j' + nat j" "i' + nat i"] by (simp add: assms)
+  then show ?thesis
+    by (auto simp: le_matrix_def)
+qed
 
-lemma move_matrix_zero_le[simp]: "0 \<le> j \<Longrightarrow> 0 \<le> i \<Longrightarrow> (0 \<le> move_matrix A j i) = ((0::('a::{order,zero}) matrix) \<le> A)"
-  apply (auto simp: le_matrix_def)
-  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
-  apply (auto)
-  done
-
-lemma move_matrix_le_move_matrix_iff[simp]: "0 \<le> j \<Longrightarrow> 0 \<le> i \<Longrightarrow> (move_matrix A j i \<le> move_matrix B j i) = (A \<le> (B::('a::{order,zero}) matrix))"
-  apply (auto simp: le_matrix_def)
-  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
-  apply (auto)
-  done  
+lemma move_matrix_le_move_matrix_iff[simp]:
+  fixes A:: "'a::{order,zero} matrix"
+  assumes "0 \<le> j" "0 \<le> i"
+  shows "(move_matrix A j i \<le> move_matrix B j i) = (A \<le> B)"
+proof -
+  have "Rep_matrix A j' i' \<le> Rep_matrix B j' i'"
+    if "\<forall>n m. \<not> int n < j \<and> \<not> int m < i \<longrightarrow> Rep_matrix A (nat (int n - j)) (nat (int m - i)) \<le> Rep_matrix B (nat (int n - j)) (nat (int m - i))"
+    for j' i'
+    using that[rule_format, of "j' + nat j" "i' + nat i"] by (simp add: assms)
+  then show ?thesis
+    by (auto simp: le_matrix_def)
+qed
 
 instantiation matrix :: ("{lattice, zero}") lattice
 begin
@@ -1434,36 +1236,21 @@
 instance matrix :: (monoid_add) monoid_add
 proof
   fix A B C :: "'a matrix"
-  show "A + B + C = A + (B + C)"    
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_assoc[simplified associative_def, THEN spec, THEN spec, THEN spec])
-    apply (simp_all add: add.assoc)
-    done
+  show "A + B + C = A + (B + C)"
+    by (simp add: add.assoc matrix_eqI plus_matrix_def)    
   show "0 + A = A"
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
-    apply (simp)
-    done
+    by (simp add: matrix_eqI plus_matrix_def)
   show "A + 0 = A"
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_zero_r_neutral [simplified zero_r_neutral_def, THEN spec])
-    apply (simp)
-    done
+    by (simp add: matrix_eqI plus_matrix_def)
 qed
 
 instance matrix :: (comm_monoid_add) comm_monoid_add
 proof
   fix A B :: "'a matrix"
   show "A + B = B + A"
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_commute[simplified commutative_def, THEN spec, THEN spec])
-    apply (simp_all add: add.commute)
-    done
+    by (simp add: add.commute matrix_eqI plus_matrix_def)
   show "0 + A = A"
-    apply (simp add: plus_matrix_def)
-    apply (rule combine_matrix_zero_l_neutral[simplified zero_l_neutral_def, THEN spec])
-    apply (simp)
-    done
+    by (simp add: plus_matrix_def matrix_eqI)
 qed
 
 instance matrix :: (group_add) group_add
@@ -1489,10 +1276,7 @@
   fix A B C :: "'a matrix"
   assume "A \<le> B"
   then show "C + A \<le> C + B"
-    apply (simp add: plus_matrix_def)
-    apply (rule le_left_combine_matrix)
-    apply (simp_all)
-    done
+    by (simp add: le_matrix_def plus_matrix_def)
 qed
   
 instance matrix :: (lattice_ab_group_add) semilattice_inf_ab_group_add ..
@@ -1502,41 +1286,28 @@
 proof
   fix A B C :: "'a matrix"
   show "A * B * C = A * (B * C)"
-    apply (simp add: times_matrix_def)
-    apply (rule mult_matrix_assoc)
-    apply (simp_all add: associative_def algebra_simps)
-    done
+    unfolding times_matrix_def
+    by (smt (verit, best) add.assoc associative_def distrib_left distrib_right group_cancel.add2 mult.assoc mult_matrix_assoc mult_not_zero)
   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 algebra_simps)
-    done
+    unfolding times_matrix_def plus_matrix_def
+    using l_distributive_matrix
+    by (metis (full_types) add.assoc add.commute associative_def commutative_def distrib_right l_distributive_def mult_not_zero)
   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 algebra_simps)
-    done
-  show "0 * A = 0" by (simp add: times_matrix_def)
-  show "A * 0 = 0" by (simp add: times_matrix_def)
-qed
+    unfolding times_matrix_def plus_matrix_def
+    using r_distributive_matrix
+    by (metis (no_types, lifting) add.assoc add.commute associative_def commutative_def distrib_left mult_zero_left mult_zero_right r_distributive_def) 
+qed (auto simp: times_matrix_def)
 
 instance matrix :: (ring) ring ..
 
 instance matrix :: (ordered_ring) ordered_ring
 proof
   fix A B C :: "'a matrix"
-  assume a: "A \<le> B"
-  assume b: "0 \<le> C"
-  from a b show "C * A \<le> C * B"
-    apply (simp add: times_matrix_def)
-    apply (rule le_left_mult)
-    apply (simp_all add: add_mono mult_left_mono)
-    done
-  from a b show "A * C \<le> B * C"
-    apply (simp add: times_matrix_def)
-    apply (rule le_right_mult)
-    apply (simp_all add: add_mono mult_right_mono)
-    done
+  assume \<section>: "A \<le> B" "0 \<le> C"
+  from \<section> show "C * A \<le> C * B"
+    by (simp add: times_matrix_def add_mono le_left_mult mult_left_mono)
+  from \<section> show "A * C \<le> B * C"
+    by (simp add: times_matrix_def add_mono le_right_mult mult_right_mono)
 qed
 
 instance matrix :: (lattice_ring) lattice_ring
@@ -1558,9 +1329,7 @@
 
 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i = 
   foldseq (+) (\<lambda>k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
-apply (simp add: times_matrix_def)
-apply (simp add: Rep_mult_matrix)
-done
+  by (simp add: times_matrix_def Rep_mult_matrix)
 
 lemma apply_matrix_add: "\<forall>x y. f (x+y) = (f x) + (f y) \<Longrightarrow> f 0 = (0::'a)
   \<Longrightarrow> apply_matrix f ((a::('a::monoid_add) matrix) + b) = (apply_matrix f a) + (apply_matrix f b)"
@@ -1570,20 +1339,18 @@
   by (simp add: matrix_eqI)
 
 lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) \<le> nrows A"
-by (simp add: times_matrix_def mult_nrows)
+  by (simp add: times_matrix_def mult_nrows)
 
 lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) \<le> ncols B"
-by (simp add: times_matrix_def mult_ncols)
+  by (simp add: times_matrix_def mult_ncols)
 
 definition
   one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
-  "one_matrix n = Abs_matrix (\<lambda>j i. if j = i & j < n then 1 else 0)"
+  "one_matrix n = Abs_matrix (\<lambda>j i. if j = i \<and> j < n then 1 else 0)"
 
-lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
-apply (simp add: one_matrix_def)
-apply (simplesubst RepAbs_matrix)
-apply (rule exI[of _ n], simp add: if_split)+
-by (simp add: if_split)
+lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i \<and> j < n) then 1 else 0)"
+  unfolding one_matrix_def
+  by (smt (verit, del_insts) RepAbs_matrix not_le)
 
 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
 proof -
@@ -1599,32 +1366,41 @@
   ultimately show "?r = n" by simp
 qed
 
-lemma one_matrix_mult_right[simp]: "ncols A \<le> n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"
+lemma one_matrix_mult_right[simp]:
+  fixes A :: "('a::semiring_1) matrix"
+  shows "ncols A \<le> n \<Longrightarrow> A * (one_matrix n) = A"
   apply (intro matrix_eqI)
   apply (simp add: times_matrix_def Rep_mult_matrix)
   apply (subst foldseq_almostzero, auto simp: ncols)
   done
 
-lemma one_matrix_mult_left[simp]: "nrows A \<le> n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"
+lemma one_matrix_mult_left[simp]: 
+  fixes A :: "('a::semiring_1) matrix"
+  shows "nrows A \<le> n \<Longrightarrow> (one_matrix n) * A = A"
   apply (intro matrix_eqI)
   apply (simp add: times_matrix_def Rep_mult_matrix)
   apply (subst foldseq_almostzero, auto simp: nrows)
   done
 
-lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
-apply (simp add: times_matrix_def)
-apply (subst transpose_mult_matrix)
-apply (simp_all add: mult.commute)
-done
+lemma transpose_matrix_mult:
+  fixes A :: "('a::comm_ring) matrix"
+  shows  "transpose_matrix (A*B) = (transpose_matrix B) * (transpose_matrix A)"
+  by (simp add: times_matrix_def transpose_mult_matrix mult.commute)
+
+lemma transpose_matrix_add:
+  fixes A :: "('a::monoid_add) matrix"
+  shows  "transpose_matrix (A+B) = transpose_matrix A + transpose_matrix B"
+  by (simp add: plus_matrix_def transpose_combine_matrix)
 
-lemma transpose_matrix_add: "transpose_matrix ((A::('a::monoid_add) matrix)+B) = transpose_matrix A + transpose_matrix B"
-by (simp add: plus_matrix_def transpose_combine_matrix)
+lemma transpose_matrix_diff:
+  fixes A :: "('a::group_add) matrix"
+  shows "transpose_matrix (A-B) = transpose_matrix A - transpose_matrix B"
+  by (simp add: diff_matrix_def transpose_combine_matrix)
 
-lemma transpose_matrix_diff: "transpose_matrix ((A::('a::group_add) matrix)-B) = transpose_matrix A - transpose_matrix B"
-by (simp add: diff_matrix_def transpose_combine_matrix)
-
-lemma transpose_matrix_minus: "transpose_matrix (-(A::('a::group_add) matrix)) = - transpose_matrix (A::'a matrix)"
-by (simp add: minus_matrix_def transpose_apply_matrix)
+lemma transpose_matrix_minus: 
+  fixes A :: "('a::group_add) matrix"
+  shows "transpose_matrix (-A) = - transpose_matrix (A::'a matrix)"
+  by (simp add: minus_matrix_def transpose_apply_matrix)
 
 definition right_inverse_matrix :: "('a::{ring_1}) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
   "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X))) \<and> nrows X \<le> ncols A" 
@@ -1636,32 +1412,25 @@
   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (left_inverse_matrix A X)"
 
 lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"
-apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
-by (simp add: right_inverse_matrix_def)
+  using ncols_mult[of A X] nrows_mult[of A X]
+  by (simp add: right_inverse_matrix_def)
 
 lemma left_inverse_matrix_dim: "left_inverse_matrix A Y \<Longrightarrow> ncols A = nrows Y"
-apply (insert ncols_mult[of Y A], insert nrows_mult[of Y A]) 
-by (simp add: left_inverse_matrix_def)
+  using ncols_mult[of Y A] nrows_mult[of Y A]
+  by (simp add: left_inverse_matrix_def)
 
 lemma left_right_inverse_matrix_unique: 
   assumes "left_inverse_matrix A Y" "right_inverse_matrix A X"
   shows "X = Y"
 proof -
-  have "Y = Y * one_matrix (nrows A)" 
-    apply (subst one_matrix_mult_right)
-    using assms
-    apply (simp_all add: left_inverse_matrix_def)
-    done
-  also have "\<dots> = Y * (A * X)" 
-    apply (insert assms)
-    apply (frule right_inverse_matrix_dim)
-    by (simp add: right_inverse_matrix_def)
+  have "Y = Y * one_matrix (nrows A)"
+    by (metis assms(1) left_inverse_matrix_def one_matrix_mult_right) 
+  also have "\<dots> = Y * (A * X)"
+    by (metis assms(2) max.idem right_inverse_matrix_def right_inverse_matrix_dim) 
   also have "\<dots> = (Y * A) * X" by (simp add: mult.assoc)
-  also have "\<dots> = X" 
-    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
+  also have "\<dots> = X"
+    using assms left_inverse_matrix_def right_inverse_matrix_def
+    by (metis left_inverse_matrix_dim max.idem one_matrix_mult_left)
   ultimately show "X = Y" by (simp)
 qed
 
@@ -1672,19 +1441,18 @@
   by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
 
 lemma zero_imp_mult_zero: "(a::'a::semiring_0) = 0 | b = 0 \<Longrightarrow> a * b = 0"
-by auto
+  by auto
 
 lemma Rep_matrix_zero_imp_mult_zero:
   "\<forall>j i k. (Rep_matrix A j k = 0) | (Rep_matrix B k i) = 0  \<Longrightarrow> A * B = (0::('a::lattice_ring) matrix)"
   by (simp add: matrix_eqI Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
 
 lemma add_nrows: "nrows (A::('a::monoid_add) matrix) \<le> u \<Longrightarrow> nrows B \<le> u \<Longrightarrow> nrows (A + B) \<le> u"
-apply (simp add: plus_matrix_def)
-apply (rule combine_nrows)
-apply (simp_all)
-done
+  by (simp add: nrows_le)
 
-lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"
+lemma move_matrix_row_mult:
+  fixes A :: "('a::semiring_0) matrix"
+  shows "move_matrix (A * B) j 0 = (move_matrix A j 0) * B"
 proof -
   have "\<And>m. \<not> int m < j \<Longrightarrow> ncols (move_matrix A j 0) \<le> max (ncols A) (nrows B)"
     by (smt (verit, best) max1 nat_int ncols_move_matrix_le)
@@ -1696,7 +1464,9 @@
     done
 qed
 
-lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"
+lemma move_matrix_col_mult:
+  fixes A :: "('a::semiring_0) matrix"
+  shows  "move_matrix (A * B) 0 i = A * (move_matrix B 0 i)"
 proof -
   have "\<And>n. \<not> int n < i \<Longrightarrow> nrows (move_matrix B 0 i) \<le> max (ncols A) (nrows B)"
     by (smt (verit, del_insts) max2 nat_int nrows_move_matrix_le)

--- a/src/HOL/Matrix_LP/SparseMatrix.thy	Fri Aug 23 23:16:53 2024 +0200
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Sat Aug 24 14:14:57 2024 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Matrix_LP/SparseMatrix.thy
-    Author:     Steven Obua
+    Author:     Steven Obua; updated to Isar by LCP
 *)
 
 theory SparseMatrix
@@ -291,7 +291,7 @@
         using sorted_sparse_row_matrix_zero apply fastforce
         apply (subst Rep_matrix_zero_imp_mult_zero)
          apply (metis Rep_move_matrix comp_1 nrows_le nrows_spvec sorted_sparse_row_vector_zero verit_comp_simplify1(3))
-        apply (simp add: )
+        apply simp
         done
     next
       case greater
@@ -434,9 +434,7 @@
 qed
 
 lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (add_spmat A B)"
-  apply (induct A B rule: add_spmat.induct)
-  apply (simp_all add: sorted_spvec_add_spvec)
-  done
+  by (induct A B rule: add_spmat.induct) (simp_all add: sorted_spvec_add_spvec)
 
 fun le_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool"
 where
@@ -464,8 +462,6 @@
   "disj_matrices A B \<longleftrightarrow>
     (\<forall>j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (\<forall>j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
 
-declare [[simp_depth_limit = 6]]
-
 lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
    by (simp add: disj_matrices_def)
 
@@ -473,73 +469,47 @@
    by (simp add: disj_matrices_def)
 
 
-lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
-  (A + B \<le> C + D) = (A \<le> C & B \<le> (D::('a::lattice_ab_group_add) matrix))"
-  apply (auto)
-  apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
-  apply (intro strip)
-  apply (erule conjE)+
-  apply (drule_tac j=j and i=i in spec2)+
-  apply (case_tac "Rep_matrix B j i = 0")
-  apply (case_tac "Rep_matrix D j i = 0")
-  apply (simp_all)
-  apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
-  apply (intro strip)
-  apply (erule conjE)+
-  apply (drule_tac j=j and i=i in spec2)+
-  apply (case_tac "Rep_matrix A j i = 0")
-  apply (case_tac "Rep_matrix C j i = 0")
-  apply (simp_all)
-  apply (erule add_mono)
-  apply (assumption)
-  done
+lemma disj_matrices_add:
+  fixes A :: "('a::lattice_ab_group_add) matrix"
+  shows  "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D 
+       \<Longrightarrow> disj_matrices B C \<Longrightarrow> (A + B \<le> C + D) = (A \<le> C \<and> B \<le> D)"
+  apply (intro iffI conjI)
+  unfolding le_matrix_def disj_matrices_def
+  apply (metis Rep_matrix_add group_cancel.rule0 order_refl)
+  apply (metis (no_types, lifting) Rep_matrix_add add_cancel_right_left dual_order.refl)
+  by (meson add_mono le_matrix_def)
 
 lemma disj_matrices_zero1[simp]: "disj_matrices 0 B"
-by (simp add: disj_matrices_def)
+  by (simp add: disj_matrices_def)
 
 lemma disj_matrices_zero2[simp]: "disj_matrices A 0"
-by (simp add: disj_matrices_def)
+  by (simp add: disj_matrices_def)
 
 lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A"
-by (auto simp: disj_matrices_def)
+  by (auto simp: disj_matrices_def)
 
 lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
   (A + B \<le> 0) = (A \<le> 0 & (B::('a::lattice_ab_group_add) matrix) \<le> 0)"
-by (rule disj_matrices_add[of A B 0 0, simplified])
- 
+  by (rule disj_matrices_add[of A B 0 0, simplified])
+
 lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
   (0 \<le> A + B) = (0 \<le> A & 0 \<le> (B::('a::lattice_ab_group_add) matrix))"
-by (rule disj_matrices_add[of 0 0 A B, simplified])
+  by (rule disj_matrices_add[of 0 0 A B, simplified])
 
 lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   (A \<le> B + C) = (A \<le> C & 0 \<le> (B::('a::lattice_ab_group_add) matrix))"
-by (auto simp: disj_matrices_add[of 0 A B C, simplified])
+  by (auto simp: disj_matrices_add[of 0 A B C, simplified])
 
 lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   (B + A \<le> C) = (A \<le> C &  (B::('a::lattice_ab_group_add) matrix) \<le> 0)"
-by (auto simp: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
+  by (auto simp: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
 
 lemma disj_sparse_row_singleton: "i \<le> j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)"
   apply (simp add: disj_matrices_def)
-  apply (rule conjI)
-  apply (rule neg_imp)
-  apply (simp)
-  apply (intro strip)
-  apply (rule sorted_sparse_row_vector_zero)
-  apply (simp_all)
-  apply (intro strip)
-  apply (rule sorted_sparse_row_vector_zero)
-  apply (simp_all)
-  done 
+  using sorted_sparse_row_vector_zero by blast
 
 lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lattice_ab_group_add) matrix) (B+C)"
-  apply (simp add: disj_matrices_def)
-  apply (auto)
-  apply (drule_tac j=j and i=i in spec2)+
-  apply (case_tac "Rep_matrix B j i = 0")
-  apply (case_tac "Rep_matrix C j i = 0")
-  apply (simp_all)
-  done
+  by (smt (verit, ccfv_SIG) Rep_matrix_add add_0 disj_matrices_def)
 
 lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lattice_ab_group_add) matrix)" 
   by (simp add: disj_matrices_x_add disj_matrices_commute)
@@ -547,97 +517,106 @@
 lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \<noteq> u | i \<noteq> v | x = 0 | y = 0)" 
   by (auto simp: disj_matrices_def)
 
-lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: 
-  "j \<le> a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
-  apply (auto simp: disj_matrices_def)
-  apply (drule nrows_notzero)
-  apply (drule less_le_trans[OF _ nrows_spvec])
-  apply (subgoal_tac "ja = j")
-  apply (simp add: sorted_sparse_row_matrix_zero)
-  apply (arith)
-  apply (rule nrows)
-  apply (rule order_trans[of _ 1 _])
-  apply (simp)
-  apply (case_tac "nat (int ja - int j) = 0")
-  apply (case_tac "ja = j")
-  apply (simp add: sorted_sparse_row_matrix_zero)
-  apply arith+
-  done
+lemma disj_move_sparse_vec_mat:
+  assumes "j \<le> a" and "sorted_spvec ((a, c) # as)"
+  shows "disj_matrices (sparse_row_matrix as) (move_matrix (sparse_row_vector b) (int j) i)"
+proof -
+  have "Rep_matrix (sparse_row_vector b) (n-j) (nat (int m - i)) = 0"
+    if "\<not> n<j" and nz: "Rep_matrix (sparse_row_matrix as) n m \<noteq> 0"
+    for n m
+  proof -
+    have "n \<noteq> j"
+      using assms sorted_sparse_row_matrix_zero nz by blast
+    with that have "j < n"  by auto
+    then show ?thesis
+      by (metis One_nat_def Suc_diff_Suc nrows nrows_spvec plus_1_eq_Suc trans_le_add1)
+  qed
+  then show ?thesis
+    by (auto simp: disj_matrices_def nat_minus_as_int)
+qed
 
 lemma disj_move_sparse_row_vector_twice:
   "j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
-  apply (auto simp: disj_matrices_def)
-  apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
-  done
-
-lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \<longrightarrow> (sorted_spvec b) \<longrightarrow> (le_spvec a b) = (sparse_row_vector a \<le> sparse_row_vector b)"
-  apply (induct a b rule: le_spvec.induct)
-  apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le 
-    disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
-  apply (rule conjI, intro strip)
-  apply (simp add: sorted_spvec_cons1)
-  apply (subst disj_matrices_add_x_le)
-  apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
-  apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
-  apply (simp, blast)
-  apply (intro strip, rule conjI, intro strip)
-  apply (simp add: sorted_spvec_cons1)
-  apply (subst disj_matrices_add_le_x)
-  apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_sparse_row_singleton[OF less_imp_le] disj_matrices_commute disj_matrices_x_add)
-  apply (blast)
-  apply (intro strip)
-  apply (simp add: sorted_spvec_cons1)
-  apply (case_tac "a=b", simp_all)
-  apply (subst disj_matrices_add)
-  apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
-  done
-
-lemma le_spvec_empty2_sparse_row[rule_format]: "sorted_spvec b \<longrightarrow> le_spvec b [] = (sparse_row_vector b \<le> 0)"
-  apply (induct b)
-  apply (simp_all add: sorted_spvec_cons1)
-  apply (intro strip)
-  apply (subst disj_matrices_add_le_zero)
-  apply (auto simp: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
-  done
+  unfolding disj_matrices_def
+  by (smt (verit, ccfv_SIG) One_nat_def Rep_move_matrix of_nat_1 le_nat_iff nrows nrows_spvec of_nat_le_iff)
 
-lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec [] b = (0 \<le> sparse_row_vector b))"
-  apply (induct b)
-  apply (simp_all add: sorted_spvec_cons1)
-  apply (intro strip)
-  apply (subst disj_matrices_add_zero_le)
-  apply (auto simp: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
-  done
+lemma le_spvec_iff_sparse_row_le:
+  "sorted_spvec a \<Longrightarrow> sorted_spvec b \<Longrightarrow> (le_spvec a b) \<longleftrightarrow> (sparse_row_vector a \<le> sparse_row_vector b)"
+proof (induct a b rule: le_spvec.induct)
+  case 1
+  then show ?case
+    by auto
+next
+  case (2 uu a as)
+  then have "sorted_spvec as"
+    by (metis sorted_spvec_cons1)
+  with 2 show ?case
+    apply (simp add: add.commute)
+    by (metis disj_matrices_add_le_zero disj_sparse_row_singleton le_refl singleton_le_zero)
+next
+  case (3 uv b bs)
+  then have "sorted_spvec bs"
+    by (metis sorted_spvec_cons1)
+  with 3 show ?case
+    apply (simp add: add.commute)
+    by (metis disj_matrices_add_zero_le disj_sparse_row_singleton le_refl singleton_ge_zero)
+next
+  case (4 i a as j b bs)
+  then obtain \<section>: "sorted_spvec as" "sorted_spvec bs"
+    by (metis sorted_spvec_cons1)
+  show ?case
+  proof (cases i j rule: linorder_cases)
+    case less
+    with 4 \<section> show ?thesis
+      apply (simp add: )
+      by (metis disj_matrices_add_le_x disj_matrices_add_x disj_matrices_commute disj_singleton_matrices disj_sparse_row_singleton less_imp_le_nat singleton_le_zero not_le)
+  next
+    case equal
+    with 4 \<section> show ?thesis
+      apply (simp add: )
+      by (metis disj_matrices_add disj_matrices_commute disj_sparse_row_singleton order_refl singleton_matrix_le)
+  next
+    case greater
+    with 4 \<section> show ?thesis
+      apply (simp add: )
+      by (metis disj_matrices_add_x disj_matrices_add_x_le disj_matrices_commute disj_singleton_matrices disj_sparse_row_singleton le_refl order_less_le singleton_ge_zero)
+  qed
+qed
 
-lemma le_spmat_iff_sparse_row_le[rule_format]: "(sorted_spvec A) \<longrightarrow> (sorted_spmat A) \<longrightarrow> (sorted_spvec B) \<longrightarrow> (sorted_spmat B) \<longrightarrow> 
+lemma le_spvec_empty2_sparse_row: 
+  "sorted_spvec b \<Longrightarrow> le_spvec b [] = (sparse_row_vector b \<le> 0)"
+  by (simp add: le_spvec_iff_sparse_row_le)
+
+lemma le_spvec_empty1_sparse_row: 
+  "(sorted_spvec b) \<Longrightarrow> (le_spvec [] b = (0 \<le> sparse_row_vector b))"
+  by (simp add: le_spvec_iff_sparse_row_le)
+
+lemma le_spmat_iff_sparse_row_le:
+  "\<lbrakk>sorted_spvec A; sorted_spmat A; sorted_spvec B; sorted_spmat B\<rbrakk> \<Longrightarrow> 
   le_spmat A B = (sparse_row_matrix A \<le> sparse_row_matrix B)"
-  apply (induct A B rule: le_spmat.induct)
-  apply (simp add: sparse_row_matrix_cons disj_matrices_add_le_zero disj_matrices_add_zero_le disj_move_sparse_vec_mat[OF order_refl] 
-    disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ 
-  apply (rule conjI, intro strip)
-  apply (simp add: sorted_spvec_cons1)
-  apply (subst disj_matrices_add_x_le)
-  apply (rule disj_matrices_add_x)
-  apply (simp add: disj_move_sparse_row_vector_twice)
-  apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
-  apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute)
-  apply (simp, blast)
-  apply (intro strip, rule conjI, intro strip)
-  apply (simp add: sorted_spvec_cons1)
-  apply (subst disj_matrices_add_le_x)
-  apply (simp add: disj_move_sparse_vec_mat[OF order_refl])
-  apply (rule disj_matrices_x_add)
-  apply (simp add: disj_move_sparse_row_vector_twice)
-  apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
-  apply (simp, blast)
-  apply (intro strip)
-  apply (case_tac "i=j")
-  apply (simp_all)
-  apply (subst disj_matrices_add)
-  apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl])
-  apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
-  done
+proof (induct A B rule: le_spmat.induct)
+  case (4 i a as j b bs)
+  then obtain \<section>: "sorted_spvec as" "sorted_spvec bs"
+    by (metis sorted_spvec_cons1)
+  show ?case
+  proof (cases i j rule: linorder_cases)
+    case less
+    with 4 \<section> show ?thesis
+      apply (simp add: sparse_row_matrix_cons le_spvec_empty2_sparse_row)
+      by (metis disj_matrices_add_le_x disj_matrices_add_x disj_matrices_commute disj_move_sparse_row_vector_twice disj_move_sparse_vec_mat int_eq_iff less_not_refl move_matrix_le_zero order_le_less)
+  next
+    case equal
+    with 4 \<section> show ?thesis
+      by (simp add: sparse_row_matrix_cons le_spvec_iff_sparse_row_le disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl] disj_matrices_add)
+  next
+    case greater
+    with 4 \<section> show ?thesis
+      apply (simp add: sparse_row_matrix_cons le_spvec_empty1_sparse_row)
+      by (metis disj_matrices_add_x disj_matrices_add_x_le disj_matrices_commute disj_move_sparse_row_vector_twice disj_move_sparse_vec_mat move_matrix_zero_le nat_int nat_less_le of_nat_0_le_iff order_refl)
+  qed
+qed (auto simp add: sparse_row_matrix_cons disj_matrices_add_le_zero disj_matrices_add_zero_le disj_move_sparse_vec_mat[OF order_refl] 
+    disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)
 
-declare [[simp_depth_limit = 999]]
 
 primrec abs_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat"
 where
@@ -792,7 +771,7 @@
 proof (induct v rule: sorted_spvec.induct)
   case (3 m x n y bs)
   then show ?case
-    apply (simp add: )
+    apply simp
     apply (subst pprt_add)
      apply (metis disj_matrices_commute disj_sparse_row_singleton order.refl fst_conv prod.sel(2) sparse_row_vector_cons)
     by (metis pprt_singleton sorted_spvec_cons1)
@@ -804,7 +783,7 @@
 proof (induct v rule: sorted_spvec.induct)
   case (3 m x n y bs)
   then show ?case
-    apply (simp add: )
+    apply simp
     apply (subst nprt_add)
     apply (metis disj_matrices_commute disj_sparse_row_singleton dual_order.refl fst_conv prod.sel(2) sparse_row_vector_cons)
     using sorted_spvec_cons1 by force
@@ -868,10 +847,10 @@
 qed
 
 lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
-by (induct v rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)
+  by (induct v rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)
 
 lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)"
-by (induct m rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)
+  by (induct m rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)
 
 lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)"
 by (induct m rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)