# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1724361988 -3600
# Node ID c8bcb14fcfa8a1d78a165fe898b8f0d0a8b540aa
# Parent  17d8b3f6d744330eabb0af85b306bff59c6d5005
Partial tidying of old proofs

diff -r 17d8b3f6d744 -r c8bcb14fcfa8 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Wed Aug 21 14:09:44 2024 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Aug 22 22:26:28 2024 +0100
@@ -22,6 +22,12 @@
 
 declare Rep_matrix_inverse[simp]
 
+lemma matrix_eqI:
+  fixes A B :: "'a::zero matrix"
+  assumes "\<And>m n. Rep_matrix A m n = Rep_matrix B m n"
+  shows "A=B"
+  using Rep_matrix_inject assms by blast
+
 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
   by (induct A) (simp add: Abs_matrix_inverse matrix_def)
 
@@ -44,8 +50,8 @@
   from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
   have "m \<notin> ?S"
     proof -
-      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max_ge [OF c])
-      moreover from d have "~(m <= Max ?S)" by (simp)
+      have "m \<in> ?S \<Longrightarrow> m \<le> Max(?S)" by (simp add: Max_ge [OF c])
+      moreover from d have "~(m \<le> Max ?S)" by (simp)
       ultimately show "m \<notin> ?S" by (auto)
     qed
   thus "Rep_matrix A m n = 0" by (simp add: nonzero_positions_def image_Collect)
@@ -62,7 +68,7 @@
 lemma transpose_infmatrix_twice[simp]: "transpose_infmatrix (transpose_infmatrix A) = A"
 by ((rule ext)+, simp)
 
-lemma transpose_infmatrix: "transpose_infmatrix (% j i. P j i) = (% j i. P i j)"
+lemma transpose_infmatrix: "transpose_infmatrix (\<lambda>j i. P j i) = (\<lambda>j i. P i j)"
   apply (rule ext)+
   by simp
 
@@ -71,7 +77,7 @@
 apply (simp add: matrix_def nonzero_positions_def image_def)
 proof -
   let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
-  let ?swap = "% pos. (snd pos, fst pos)"
+  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)
@@ -102,43 +108,32 @@
   ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
 qed
 
-lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b" by auto
+lemma infmatrixforward: "(x::'a infmatrix) = y \<Longrightarrow> \<forall> a b. x a b = y a b"
+  by auto
 
 lemma transpose_infmatrix_inject: "(transpose_infmatrix A = transpose_infmatrix B) = (A = B)"
-apply (auto)
-apply (rule ext)+
-apply (simp add: transpose_infmatrix)
-apply (drule infmatrixforward)
-apply (simp)
-done
+  by (metis transpose_infmatrix_twice)
 
 lemma transpose_matrix_inject: "(transpose_matrix A = transpose_matrix B) = (A = B)"
-apply (simp add: transpose_matrix_def)
-apply (subst Rep_matrix_inject[THEN sym])+
-apply (simp only: transpose_infmatrix_closed transpose_infmatrix_inject)
-done
+  unfolding transpose_matrix_def o_def
+  by (metis Rep_matrix_inject transpose_infmatrix_closed transpose_infmatrix_inject)
 
 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
-by (simp add: transpose_matrix_def)
+  by (simp add: transpose_matrix_def)
 
 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
-by (simp add: transpose_matrix_def)
+  by (simp add: transpose_matrix_def)
 
 lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A"
-by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
+  by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
 
 lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A"
-by (simp add: nrows_def ncols_def nonzero_positions_def transpose_matrix_def image_def)
+  by (metis nrows_transpose transpose_transpose_id)
 
-lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0"
-proof -
-  assume "ncols A <= n"
-  then have "nrows (transpose_matrix A) <= n" by (simp)
-  then have "Rep_matrix (transpose_matrix A) n m = 0" by (rule nrows)
-  thus "Rep_matrix A m n = 0" by (simp add: transpose_matrix_def)
-qed
+lemma ncols: "ncols A \<le> n \<Longrightarrow> Rep_matrix A m n = 0"
+  by (metis nrows nrows_transpose transpose_matrix)
 
-lemma ncols_le: "(ncols A <= n) = (\<forall>j i. n <= i \<longrightarrow> (Rep_matrix A j i) = 0)" (is "_ = ?st")
+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)
@@ -146,8 +141,8 @@
   let ?p = "snd`?P"
   have a:"finite ?p" by (simp add: finite_nonzero_positions)
   let ?m = "Max ?p"
-  assume "~(Suc (?m) <= n)"
-  then have b:"n <= ?m" by (simp)
+  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)
@@ -158,76 +153,60 @@
   ultimately show "False" using b by (simp)
 qed
 
-lemma less_ncols: "(n < ncols A) = (\<exists>j i. n <= i & (Rep_matrix A j i) \<noteq> 0)"
+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 <= a))" by arith
+  have a: "!! (a::nat) b. (a < b) = (~(b \<le> a))" by arith
   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)"
+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 <= m")
+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)
 
-lemma nrows_le: "(nrows A <= n) = (\<forall>j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" (is ?s)
+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 <= n) = (ncols (transpose_matrix A) <= n)" by (simp)
-  also have "\<dots> = (\<forall>j i. n <= i \<longrightarrow> (Rep_matrix (transpose_matrix A) j i = 0))" by (rule ncols_le)
-  also have "\<dots> = (\<forall>j i. n <= i \<longrightarrow> (Rep_matrix A i j) = 0)" by (simp)
-  finally show "(nrows A <= n) = (\<forall>j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
+  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
 
-lemma less_nrows: "(m < nrows A) = (\<exists>j i. m <= j & (Rep_matrix A j i) \<noteq> 0)"
+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 <= a))" by arith
+  have a: "!! (a::nat) b. (a < b) = (~(b \<le> a))" by arith
   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)"
-apply (auto)
-apply (subgoal_tac "nrows A <= m")
-apply (simp)
-apply (simp add: nrows_le)
-apply (drule_tac x="nrows A" in spec)
-by (simp add: nrows)
+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)
 
 lemma nrows_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> m < nrows A"
-apply (case_tac "nrows A <= m")
-apply (simp_all add: nrows)
-done
+  by (meson leI nrows)
 
 lemma ncols_notzero: "Rep_matrix A m n \<noteq> 0 \<Longrightarrow> n < ncols A"
-apply (case_tac "ncols A <= n")
-apply (simp_all add: ncols)
-done
+  by (meson leI ncols)
 
 lemma finite_natarray1: "finite {x. x < (n::nat)}"
-apply (induct n)
-apply (simp)
-proof -
-  fix n
-  have "{x. x < Suc n} = insert n {x. x < n}"  by (rule set_eqI, simp, arith)
-  moreover assume "finite {x. x < n}"
-  ultimately show "finite {x. x < Suc n}" by (simp)
-qed
+  by (induct n) auto
 
 lemma finite_natarray2: "finite {(x, y). x < (m::nat) & y < (n::nat)}"
-by simp
+  by simp
 
 lemma RepAbs_matrix:
-  assumes aem: "\<exists>m. \<forall>j i. m <= j \<longrightarrow> x j i = 0" (is ?em) and aen:"\<exists>n. \<forall>j i. (n <= i \<longrightarrow> x j i = 0)" (is ?en)
+  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)
   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 <= j \<longrightarrow> x j i = 0" by (blast)
-  from aen obtain n where b: "\<forall>j i. n <= i \<longrightarrow> x j i = 0" by (blast)
+  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 <= a) \<Longrightarrow> a < m" by (arith)
+  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)
@@ -242,28 +221,28 @@
 qed
 
 definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where
-  "apply_infmatrix f == % A. (% j i. f (A j i))"
+  "apply_infmatrix f == \<lambda>A. (\<lambda>j i. f (A j i))"
 
 definition apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix" where
-  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
+  "apply_matrix f == \<lambda>A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
 
 definition combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix" where
-  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
+  "combine_infmatrix f == \<lambda>A B. (\<lambda>j i. f (A j i) (B j i))"
 
 definition combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix" where
-  "combine_matrix f == % A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
+  "combine_matrix f == \<lambda>A B. Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))"
 
 lemma expand_apply_infmatrix[simp]: "apply_infmatrix f A j i = f (A j i)"
-by (simp add: apply_infmatrix_def)
+  by (simp add: apply_infmatrix_def)
 
 lemma expand_combine_infmatrix[simp]: "combine_infmatrix f A B j i = f (A j i) (B j i)"
-by (simp add: combine_infmatrix_def)
+  by (simp add: combine_infmatrix_def)
 
 definition commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool" where
-"commutative f == \<forall>x y. f x y = f y x"
+  "commutative f == \<forall>x y. f x y = f y x"
 
 definition associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool" where
-"associative f == \<forall>x y z. f (f x y) z = f x (f y z)"
+  "associative f == \<forall>x y z. f (f x y) z = f x (f y z)"
 
 text\<open>
 To reason about associativity and commutativity of operations on matrices,
@@ -291,10 +270,10 @@
 \<close>
 
 lemma nonzero_positions_combine_infmatrix[simp]: "f 0 0 = 0 \<Longrightarrow> nonzero_positions (combine_infmatrix f A B) \<subseteq> (nonzero_positions A) \<union> (nonzero_positions B)"
-by (rule subsetI, simp add: nonzero_positions_def combine_infmatrix_def, auto)
+  by (smt (verit) UnCI expand_combine_infmatrix mem_Collect_eq nonzero_positions_def subsetI)
 
 lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
-by (insert Rep_matrix [of A], simp add: matrix_def)
+  by (simp add: finite_nonzero_positions)
 
 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)"
@@ -315,10 +294,10 @@
 by (simp_all)
 
 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)
+  by (simp add: associative_def combine_infmatrix_def)
 
 lemma comb: "f = g \<Longrightarrow> x = y \<Longrightarrow> f x = g y"
-by (auto)
+  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)
@@ -331,16 +310,16 @@
 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) <= max (nrows A) (nrows B)"
+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)
 
-lemma combine_ncols_max: "f 0 0 = 0 \<Longrightarrow> ncols (combine_matrix f A B) <= max (ncols A) (ncols B)"
+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)
 
-lemma combine_nrows: "f 0 0 = 0 \<Longrightarrow> nrows A <= q \<Longrightarrow> nrows B <= q \<Longrightarrow> nrows(combine_matrix f A B) <= q"
+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)
 
-lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A <= q \<Longrightarrow> ncols B <= q \<Longrightarrow> ncols(combine_matrix f A B) <= q"
+lemma combine_ncols: "f 0 0 = 0 \<Longrightarrow> ncols A \<le> q \<Longrightarrow> ncols B \<le> q \<Longrightarrow> ncols(combine_matrix f A B) \<le> q"
   by (simp add: ncols_le)
 
 definition zero_r_neutral :: "('a \<Rightarrow> 'b::zero \<Rightarrow> 'a) \<Rightarrow> bool" where
@@ -355,7 +334,7 @@
 primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
 where
   "foldseq f s 0 = s 0"
-| "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
+| "foldseq f s (Suc n) = f (s 0) (foldseq f (\<lambda>k. s(Suc k)) n)"
 
 primrec foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
 where
@@ -365,28 +344,28 @@
 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
 proof -
   assume a:"associative f"
-  then have sublemma: "\<And>n. \<forall>N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
+  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 <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s 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 <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
+      show "\<forall>N s. N \<le> 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
     next
       fix n
-      assume b: "\<forall>N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
-      have c:"\<And>N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
-      show "\<forall>N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t 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 <= Suc n"
+        assume Nsuc: "N \<le> Suc n"
         show "foldseq f t N = foldseq_transposed f t N"
         proof cases
-          assume "N <= n"
+          assume "N \<le> n"
           then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
         next
-          assume "~(N <= n)"
+          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 <= n" by arith
+          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)
@@ -400,9 +379,9 @@
             apply (subst assocf)
             proof -
               fix m
-              assume "n = Suc m & Suc m <= n"
-              then have mless: "Suc m <= n" by arith
-              then have step1: "foldseq_transposed f (% k. t (Suc k)) m = foldseq f (% k. t (Suc k)) m" (is "?T1 = ?T2")
+              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
@@ -419,18 +398,18 @@
     show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
   qed
 
-lemma foldseq_distr: "\<lbrakk>associative f; commutative f\<rbrakk> \<Longrightarrow> foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)"
+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)"
 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 (%k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n))"
+  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)
-  then show "foldseq f (% k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
+  then show "foldseq f (\<lambda>k. f (u k) (v k)) n = f (foldseq f u n) (foldseq f v n)" by simp
 qed
 
 theorem "\<lbrakk>associative f; associative g; \<forall>a b c d. g (f a b) (f c d) = f (g a c) (g b d); \<exists>x y. (f x) \<noteq> (f y); \<exists>x y. (g x) \<noteq> (g y); f x x = x; g x x = x\<rbrakk> \<Longrightarrow> f=g | (\<forall>y. f y x = y) | (\<forall>y. g y x = y)"
@@ -452,10 +431,10 @@
 *)
 
 lemma foldseq_zero:
-assumes fz: "f 0 0 = 0" and sz: "\<forall>i. i <= n \<longrightarrow> s i = 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 <= n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s n = 0"
+  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)
@@ -463,7 +442,7 @@
 qed
 
 lemma foldseq_significant_positions:
-  assumes p: "\<forall>i. i <= N \<longrightarrow> S i = T i"
+  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"
@@ -485,12 +464,12 @@
 qed
 
 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"
+  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 <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
+  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 <= 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"
+  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)
@@ -504,12 +483,12 @@
     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 <= na"
-      from suba have subc:"!! m s. m <= 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
+      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 (% k. s(Suc k)) na"
-        by (rule subc[of m "% k. s(Suc k)", THEN sym], simp add: subb)
-      from subb have sube: "m \<noteq> 0 \<Longrightarrow> \<exists>mm. m = Suc mm & mm <= na" by arith
+        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)
@@ -525,30 +504,20 @@
 qed
 
 lemma foldseq_zerotail:
-  assumes
-  fz: "f 0 0 = 0"
-  and sz: "\<forall>i.  n <= i \<longrightarrow> s i = 0"
-  and nm: "n <= m"
-  shows
-  "foldseq f s n = foldseq f s m"
-proof -
-  show "foldseq f s n = foldseq f s m"
-    apply (simp add: foldseq_tail[OF nm, of f s])
-    apply (rule foldseq_significant_positions)
-    apply (auto)
-    apply (subst foldseq_zero)
-    by (simp add: fz sz)+
-qed
+  assumes fz: "f 0 0 = 0" and sz: "\<forall>i.  n \<le> i \<longrightarrow> s i = 0" and nm: "n \<le> m"
+  shows "foldseq f s n = foldseq f s m"
+  unfolding foldseq_tail[OF nm]
+  by (metis (no_types, lifting) foldseq_zero fz le_add2 linorder_not_le sz)
 
 lemma foldseq_zerotail2:
   assumes "\<forall>x. f x 0 = x"
   and "\<forall>i. n < i \<longrightarrow> s i = 0"
-  and nm: "n <= m"
+  and nm: "n \<le> 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 <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> \<exists>k. m-n = Suc k" by arith
-  have c: "0 <= m" by simp
+  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])
@@ -567,7 +536,7 @@
 qed
 
 lemma foldseq_zerostart:
-  "\<forall>x. f 0 (f 0 x) = f 0 x \<Longrightarrow> \<forall>i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
+  "\<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))"
@@ -577,16 +546,16 @@
     proof -
       fix n
       fix s
-      have a:"foldseq f s (Suc (Suc n)) = f (s 0) (foldseq f (% k. s(Suc k)) (Suc n))" by simp
+      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 <= Suc n \<longrightarrow> s i = 0"
+      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 <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
+  then show "\<forall>i. i \<le> n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
 qed
 
 lemma foldseq_zerostart2:
@@ -595,7 +564,7 @@
   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 <= l)" by arith
+  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")
@@ -611,7 +580,7 @@
 
 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 <= n) then (s j) else 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
@@ -627,20 +596,20 @@
 
 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"
+  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 (% x. g(s x)) n"
+  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="% k. s (Suc k)" in spec)
+    apply (drule_tac x="\<lambda>k. s (Suc k)" in spec)
     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
-  "mult_matrix_n n fmul fadd A B == Abs_matrix(% j i. foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n)"
+  "mult_matrix_n n fmul fadd A B == Abs_matrix(\<lambda>j i. foldseq fadd (\<lambda>k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n)"
 
 definition mult_matrix :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix" where
   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
@@ -657,7 +626,7 @@
 qed
 
 lemma mult_matrix_nm:
-  assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
+  assumes "ncols A \<le> n" "nrows B \<le> n" "ncols A \<le> m" "nrows B \<le> 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 assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B"
@@ -676,8 +645,8 @@
 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"
 
-lemma max1: "!! a x y. (a::nat) <= x \<Longrightarrow> a <= max x y" by (arith)
-lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
+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)
 
 lemma r_distributive_matrix:
  assumes
@@ -775,13 +744,13 @@
 
 lemma zero_matrix_def_nrows[simp]: "nrows 0 = 0"
 proof -
-  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
+  have a:"!! (x::nat). x \<le> 0 \<Longrightarrow> x = 0" by (arith)
   show "nrows 0 = 0" by (rule a, subst nrows_le, simp)
 qed
 
 lemma zero_matrix_def_ncols[simp]: "ncols 0 = 0"
 proof -
-  have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
+  have a:"!! (x::nat). x \<le> 0 \<Longrightarrow> x = 0" by (arith)
   show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
 qed
 
@@ -821,26 +790,23 @@
   by (simp add: zero_matrix_def)
 
 lemma transpose_matrix_zero[simp]: "transpose_matrix 0 = 0"
-apply (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix)
-apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
-apply (simp add: RepAbs_matrix)
-done
+  by (simp add: transpose_matrix_def zero_matrix_def RepAbs_matrix transpose_infmatrix)
 
-lemma apply_zero_matrix_def[simp]: "apply_matrix (% x. 0) A = 0"
+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)
 
 definition singleton_matrix :: "nat \<Rightarrow> nat \<Rightarrow> ('a::zero) \<Rightarrow> 'a matrix" where
-  "singleton_matrix j i a == Abs_matrix(% m n. if j = m & i = n then a else 0)"
+  "singleton_matrix j i a == Abs_matrix(\<lambda>m n. if j = m & 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(% 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)))"
+  "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)))"
 
 definition take_rows :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
-  "take_rows A r == Abs_matrix(% j i. if (j < r) then (Rep_matrix A j i) else 0)"
+  "take_rows A r == Abs_matrix(\<lambda>j i. if (j < r) then (Rep_matrix A j i) else 0)"
 
 definition take_columns :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
-  "take_columns A c == Abs_matrix(% j i. if (i < c) then (Rep_matrix A j i) else 0)"
+  "take_columns A c == Abs_matrix(\<lambda>j i. if (i < c) then (Rep_matrix A j i) else 0)"
 
 definition column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix" where
   "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
@@ -857,17 +823,14 @@
 by (subst RepAbs_matrix, rule exI[of _ "Suc j"], simp, rule exI[of _ "Suc i"], simp+)+
 
 lemma apply_singleton_matrix[simp]: "f 0 = 0 \<Longrightarrow> apply_matrix f (singleton_matrix j i x) = (singleton_matrix j i (f x))"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
 lemma singleton_matrix_zero[simp]: "singleton_matrix j i 0 = 0"
   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+
+  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)
@@ -909,9 +872,7 @@
 by simp
 
 lemma transpose_singleton[simp]: "transpose_matrix (singleton_matrix j i a) = singleton_matrix i j a"
-apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
 lemma Rep_move_matrix[simp]:
   "Rep_matrix (move_matrix A y x) j i =
@@ -926,27 +887,17 @@
 by (simp add: move_matrix_def)
 
 lemma move_matrix_ortho: "move_matrix A j i = move_matrix (move_matrix A j 0) 0 i"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
 lemma transpose_move_matrix[simp]:
   "transpose_matrix (move_matrix A x y) = move_matrix (transpose_matrix A) y x"
-apply (subst Rep_matrix_inject[symmetric], (rule ext)+)
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
-lemma move_matrix_singleton[simp]: "move_matrix (singleton_matrix u v x) j i = 
+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 (subst Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply (case_tac "j + int u < 0")
-  apply (simp, arith)
-  apply (case_tac "i + int v < 0")
-  apply (simp, arith)
-  apply simp
-  apply arith
+  apply (intro matrix_eqI)
+  apply (split if_split)
+  apply (auto simp: split: if_split_asm)
   done
 
 lemma Rep_take_columns[simp]:
@@ -975,15 +926,11 @@
   "Rep_matrix (row_of_matrix A r) j i = (if j = 0 then (Rep_matrix A r i) else 0)"
   by (simp add: row_of_matrix_def)
 
-lemma column_of_matrix: "ncols A <= n \<Longrightarrow> column_of_matrix A n = 0"
-apply (subst Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-by (simp add: ncols)
+lemma column_of_matrix: "ncols A \<le> n \<Longrightarrow> column_of_matrix A n = 0"
+  by (simp add: matrix_eqI ncols)
 
-lemma row_of_matrix: "nrows A <= n \<Longrightarrow> row_of_matrix A n = 0"
-apply (subst Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-by (simp add: nrows)
+lemma row_of_matrix: "nrows A \<le> n \<Longrightarrow> row_of_matrix A n = 0"
+  by (simp add: matrix_eqI nrows)
 
 lemma mult_matrix_singleton_right[simp]:
   assumes
@@ -991,7 +938,7 @@
   "\<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 (% x. fmul x e) (move_matrix (column_of_matrix A j) 0 (int i))"
+  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)
@@ -1012,37 +959,33 @@
   "\<forall>a. fmul a 0 = 0"
   "\<forall>a. fadd a 0 = a"
   "\<forall>a. fadd 0 a = a"
-  and contraprems:
-  "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
-  shows
-  "A = B"
+  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)"
-    apply (rule contrapos_np[of "False"], simp+)
-    apply (insert b[of "Rep_matrix A" "Rep_matrix B"], simp)
-    by (simp add: Rep_matrix_inject a)
+    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
   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"
   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: assms)
-  have "~(?comp A ?S = ?comp B ?S)"
-    apply (rule notI)
-    apply (simp add: fprems eprops)
-    apply (simp add: Rep_matrix_inject[THEN sym])
-    apply (drule d[of _ _ "J"], drule d[of _ _ "0"])
-    by (simp add: e c eprops)
+  have e: "(\<lambda>x. fmul x e) 0 = 0" by (simp add: assms)
+  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 (simp add: fprems eprops Rep_matrix_inject)
   with contraprems show "False" by simp
 qed
 
 definition foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
-  "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
+  "foldmatrix f g A m n == foldseq_transposed g (\<lambda>j. foldseq f (A j) n) m"
 
 definition foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
-  "foldmatrix_transposed f g A m n == foldseq g (% j. foldseq_transposed f (A j) n) m"
+  "foldmatrix_transposed f g A m n == foldseq g (\<lambda>j. foldseq_transposed f (A j) n) m"
 
 lemma foldmatrix_transpose:
   assumes
@@ -1055,13 +998,13 @@
     apply (induct n)
     apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+
     apply (auto)
-    by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
+    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="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)
+    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: foldmatrix_def foldmatrix_transposed_def)
 qed
 
@@ -1071,7 +1014,7 @@
   "associative g"
   "\<forall>a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
 shows
-  "foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
+  "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])
   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)
 
@@ -1123,14 +1066,14 @@
 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) <= nat((int (nrows A)) + j)"
-  apply (auto simp add: nrows_le)
+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
 
-lemma ncols_move_matrix_le: "ncols (move_matrix A j i) <= nat((int (ncols A)) + i)"
-  apply (auto simp add: ncols_le)
+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
@@ -1152,14 +1095,13 @@
   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], insert assms, simp_all)
-  have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
-    using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all)
+  have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n)  x = foldseq fadd1 (\<lambda>k. fmul2 (s k) x) n"
+    by (rule_tac g1 = "\<lambda>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 (\<lambda>k. fmul1 x (s k)) n"
+    using assms by (rule_tac g1 = "\<lambda>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 ?thesis
-    apply (simp add: Rep_matrix_inject[THEN sym])
-    apply (rule ext)+
+    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)+
@@ -1236,14 +1178,10 @@
 qed
 
 lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
-apply (simp add: Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-by simp
+  by (simp add: matrix_eqI)
 
 lemma transpose_combine_matrix: "f 0 0 = 0 \<Longrightarrow> transpose_matrix (combine_matrix f A B) = combine_matrix f (transpose_matrix A) (transpose_matrix B)"
-apply (simp add: Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-by simp
+  by (simp add: matrix_eqI)
 
 lemma Rep_mult_matrix:
   assumes
@@ -1252,7 +1190,7 @@
   "fadd 0 0 = 0"
   shows
   "Rep_matrix(mult_matrix fmul fadd A B) j i =
-  foldseq fadd (% 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)) (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)
@@ -1268,21 +1206,14 @@
   "\<forall>x y. fmul y x = fmul x y"
   shows
   "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)+
   using assms
-  apply (simp add: Rep_mult_matrix ac_simps)
-  done
+  by (simp add: matrix_eqI Rep_mult_matrix ac_simps) 
 
 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])
-apply (rule ext)+
-by simp
+  by (simp add: matrix_eqI)
 
 lemma take_columns_transpose_matrix: "take_columns (transpose_matrix A) n = transpose_matrix (take_rows A n)"
-apply (simp add: Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-by simp
+  by (simp add: matrix_eqI)
 
 instantiation matrix :: ("{zero, ord}") ord
 begin
@@ -1298,82 +1229,79 @@
 end
 
 instance matrix :: ("{zero, order}") order
-apply intro_classes
-apply (simp_all add: le_matrix_def less_def)
-apply (auto)
-apply (drule_tac x=j in spec, drule_tac x=j in spec)
-apply (drule_tac x=i in spec, drule_tac x=i in spec)
-apply (simp)
-apply (simp add: Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
-apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
-apply simp
-done
+proof
+  fix x y z :: "'a matrix"
+  assume "x \<le> y" "y \<le> z"
+  show "x \<le> z"
+    by (meson \<open>x \<le> y\<close> \<open>y \<le> z\<close> le_matrix_def order_trans)
+next
+  fix x y :: "'a matrix"
+  assume "x \<le> y" "y \<le> x"
+  show "x = y"
+    by (meson \<open>x \<le> y\<close> \<open>y \<le> x\<close> le_matrix_def matrix_eqI order_antisym)
+qed (auto simp: less_def le_matrix_def)
 
 lemma le_apply_matrix:
   assumes
   "f 0 = 0"
-  "\<forall>x y. x <= y \<longrightarrow> f x <= f y"
-  "(a::('a::{ord, zero}) matrix) <= b"
-  shows
-  "apply_matrix f a <= apply_matrix f b"
+  "\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y"
+  "(a::('a::{ord, zero}) matrix) \<le> b"
+  shows "apply_matrix f a \<le> apply_matrix f b"
   using assms by (simp add: le_matrix_def)
 
 lemma le_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "\<forall>a b c d. a <= b & c <= d \<longrightarrow> f a c <= f b d"
-  "A <= B"
-  "C <= D"
-  shows
-  "combine_matrix f A C <= combine_matrix f B D"
+  "\<forall>a b c d. a \<le> b & 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"
   using assms by (simp add: le_matrix_def)
 
 lemma le_left_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "\<forall>a b c. a <= b \<longrightarrow> f c a <= f c b"
-  "A <= B"
+  "\<forall>a b c. a \<le> b \<longrightarrow> f c a \<le> f c b"
+  "A \<le> B"
   shows
-  "combine_matrix f C A <= combine_matrix f C B"
+  "combine_matrix f C A \<le> combine_matrix f C B"
   using assms by (simp add: le_matrix_def)
 
 lemma le_right_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "\<forall>a b c. a <= b \<longrightarrow> f a c <= f b c"
-  "A <= B"
+  "\<forall>a b c. a \<le> b \<longrightarrow> f a c \<le> f b c"
+  "A \<le> B"
   shows
-  "combine_matrix f A C <= combine_matrix f B C"
+  "combine_matrix f A C \<le> combine_matrix f B C"
   using assms by (simp add: le_matrix_def)
 
-lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
+lemma le_transpose_matrix: "(A \<le> B) = (transpose_matrix A \<le> transpose_matrix B)"
   by (simp add: le_matrix_def, auto)
 
 lemma le_foldseq:
   assumes
-  "\<forall>a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
-  "\<forall>i. i <= n \<longrightarrow> s i <= t i"
+  "\<forall>a b c d . a \<le> b & 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 <= foldseq f t n"
+  "foldseq f s n \<le> foldseq f t n"
 proof -
-  have "\<forall>s t. (\<forall>i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n"
+  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)
-  then show "foldseq f s n <= foldseq f t n" using assms by simp
+  then show "foldseq f s n \<le> foldseq f t n" using assms by simp
 qed
 
 lemma le_left_mult:
   assumes
-  "\<forall>a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
-  "\<forall>c a b.   0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
+  "\<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. fmul 0 a = 0"
   "\<forall>a. fmul a 0 = 0"
   "fadd 0 0 = 0"
-  "0 <= C"
-  "A <= B"
+  "0 \<le> C"
+  "A \<le> B"
   shows
-  "mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
+  "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)
@@ -1384,15 +1312,15 @@
 
 lemma le_right_mult:
   assumes
-  "\<forall>a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
-  "\<forall>c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
+  "\<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. fmul 0 a = 0"
   "\<forall>a. fmul a 0 = 0"
   "fadd 0 0 = 0"
-  "0 <= C"
-  "A <= B"
+  "0 \<le> C"
+  "A \<le> B"
   shows
-  "mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
+  "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)
@@ -1404,10 +1332,10 @@
 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 <= singleton_matrix j i b) = (a <= (b::_::order))"
-  by (auto simp add: le_matrix_def)
+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 <= 0) = (x <= (0::'a::{order,zero}))"
+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)
@@ -1415,7 +1343,7 @@
   apply (simp add: le_matrix_def)
   done
 
-lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
+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)
@@ -1423,20 +1351,20 @@
   apply (simp add: le_matrix_def)
   done
 
-lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
-  apply (auto simp add: le_matrix_def)
+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]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
-  apply (auto simp add: le_matrix_def)
+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 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))"
-  apply (auto simp add: le_matrix_def)
+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  
@@ -1449,7 +1377,7 @@
 definition "sup = combine_matrix sup"
 
 instance
-  by standard (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
+  by standard (auto simp: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
 
 end
 
@@ -1542,25 +1470,25 @@
 proof
   fix A B :: "'a matrix"
   show "- A + A = 0" 
-    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
+    by (simp add: plus_matrix_def minus_matrix_def matrix_eqI)
   show "A + - B = A - B"
-    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext)
+    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def matrix_eqI)
 qed
 
 instance matrix :: (ab_group_add) ab_group_add
 proof
   fix A B :: "'a matrix"
   show "- A + A = 0" 
-    by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
+    by (simp add: plus_matrix_def minus_matrix_def matrix_eqI)
   show "A - B = A + - B" 
-    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
+    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def matrix_eqI)
 qed
 
 instance matrix :: (ordered_ab_group_add) ordered_ab_group_add
 proof
   fix A B C :: "'a matrix"
-  assume "A <= B"
-  then show "C + A <= C + B"
+  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)
@@ -1618,38 +1546,38 @@
     by (simp add: abs_matrix_def)
 qed
 
+instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
+proof
+  show "\<And>a:: 'a matrix. \<bar>a\<bar> = sup a (- a)"
+    by (simp add: abs_matrix_def)
+qed
+
 lemma Rep_matrix_add[simp]:
   "Rep_matrix ((a::('a::monoid_add)matrix)+b) j i  = (Rep_matrix a j i) + (Rep_matrix b j i)"
   by (simp add: plus_matrix_def)
 
 lemma Rep_matrix_mult: "Rep_matrix ((a::('a::semiring_0) matrix) * b) j i = 
-  foldseq (+) (% k.  (Rep_matrix a j k) * (Rep_matrix b k i)) (max (ncols a) (nrows b))"
+  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
 
 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)"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
 lemma singleton_matrix_add: "singleton_matrix j i ((a::_::monoid_add)+b) = (singleton_matrix j i a) + (singleton_matrix j i b)"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
-lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) <= nrows A"
+lemma nrows_mult: "nrows ((A::('a::semiring_0) matrix) * B) \<le> nrows A"
 by (simp add: times_matrix_def mult_nrows)
 
-lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) <= ncols B"
+lemma ncols_mult: "ncols ((A::('a::semiring_0) matrix) * B) \<le> ncols B"
 by (simp add: times_matrix_def mult_ncols)
 
 definition
   one_matrix :: "nat \<Rightarrow> ('a::{zero,one}) matrix" where
-  "one_matrix n = Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
+  "one_matrix n = Abs_matrix (\<lambda>j i. if j = i & 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)
@@ -1659,33 +1587,29 @@
 
 lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
 proof -
-  have "?r <= n" by (simp add: nrows_le)
-  moreover have "n <= ?r" by (simp add:le_nrows, arith)
+  have "?r \<le> n" by (simp add: nrows_le)
+  moreover have "n \<le> ?r" by (simp add:le_nrows, arith)
   ultimately show "?r = n" by simp
 qed
 
 lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
 proof -
-  have "?r <= n" by (simp add: ncols_le)
-  moreover have "n <= ?r" by (simp add: le_ncols, arith)
+  have "?r \<le> n" by (simp add: ncols_le)
+  moreover have "n \<le> ?r" by (simp add: le_ncols, arith)
   ultimately show "?r = n" by simp
 qed
 
-lemma one_matrix_mult_right[simp]: "ncols A <= n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (one_matrix n) = A"
-apply (subst Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-apply (simp add: times_matrix_def Rep_mult_matrix)
-apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
-apply (simp_all)
-by (simp add: ncols)
+lemma one_matrix_mult_right[simp]: "ncols A \<le> n \<Longrightarrow> (A::('a::{semiring_1}) matrix) * (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 <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"
-apply (subst Rep_matrix_inject[THEN sym])
-apply (rule ext)+
-apply (simp add: times_matrix_def Rep_mult_matrix)
-apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
-apply (simp_all)
-by (simp add: nrows)
+lemma one_matrix_mult_left[simp]: "nrows A \<le> n \<Longrightarrow> (one_matrix n) * A = (A::('a::semiring_1) matrix)"
+  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)
@@ -1742,7 +1666,7 @@
 qed
 
 lemma inverse_matrix_inject: "\<lbrakk> inverse_matrix A X; inverse_matrix A Y \<rbrakk> \<Longrightarrow> X = Y"
-  by (auto simp add: inverse_matrix_def left_right_inverse_matrix_unique)
+  by (auto simp: inverse_matrix_def left_right_inverse_matrix_unique)
 
 lemma one_matrix_inverse: "inverse_matrix (one_matrix n) (one_matrix n)"
   by (simp add: inverse_matrix_def left_inverse_matrix_def right_inverse_matrix_def)
@@ -1752,44 +1676,40 @@
 
 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)"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (auto simp add: Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
-done
+  by (simp add: matrix_eqI Rep_matrix_mult foldseq_zero zero_imp_mult_zero)
 
-lemma add_nrows: "nrows (A::('a::monoid_add) matrix) <= u \<Longrightarrow> nrows B <= u \<Longrightarrow> nrows (A + B) <= u"
+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
 
 lemma move_matrix_row_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) j 0 = (move_matrix A j 0) * B"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (auto simp add: Rep_matrix_mult foldseq_zero)
-apply (rule_tac foldseq_zerotail[symmetric])
-apply (auto simp add: nrows zero_imp_mult_zero max2)
-apply (rule order_trans)
-apply (rule ncols_move_matrix_le)
-apply (simp add: max1)
-done
+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)
+  then show ?thesis
+    apply (intro matrix_eqI)
+    apply (auto simp: Rep_matrix_mult foldseq_zero)
+    apply (rule_tac foldseq_zerotail[symmetric])
+      apply (auto simp: nrows zero_imp_mult_zero max2)
+    done
+qed
 
 lemma move_matrix_col_mult: "move_matrix ((A::('a::semiring_0) matrix) * B) 0 i = A * (move_matrix B 0 i)"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (auto simp add: Rep_matrix_mult foldseq_zero)
-apply (rule_tac foldseq_zerotail[symmetric])
-apply (auto simp add: ncols zero_imp_mult_zero max1)
-apply (rule order_trans)
-apply (rule nrows_move_matrix_le)
-apply (simp add: max2)
-done
+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)
+  then show ?thesis
+    apply (intro matrix_eqI)
+    apply (auto simp: Rep_matrix_mult foldseq_zero)
+    apply (rule_tac foldseq_zerotail[symmetric])
+      apply (auto simp: ncols zero_imp_mult_zero max1)
+    done
+  qed
 
 lemma move_matrix_add: "((move_matrix (A + B) j i)::(('a::monoid_add) matrix)) = (move_matrix A j i) + (move_matrix B j i)" 
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (simp)
-done
+  by (simp add: matrix_eqI)
 
 lemma move_matrix_mult: "move_matrix ((A::('a::semiring_0) matrix)*B) j i = (move_matrix A j 0) * (move_matrix B 0 i)"
 by (simp add: move_matrix_ortho[of "A*B"] move_matrix_col_mult move_matrix_row_mult)
@@ -1798,24 +1718,21 @@
   "scalar_mult a m == apply_matrix ((*) a) m"
 
 lemma scalar_mult_zero[simp]: "scalar_mult y 0 = 0" 
-by (simp add: scalar_mult_def)
+  by (simp add: scalar_mult_def)
 
 lemma scalar_mult_add: "scalar_mult y (a+b) = (scalar_mult y a) + (scalar_mult y b)"
-by (simp add: scalar_mult_def apply_matrix_add algebra_simps)
+  by (simp add: scalar_mult_def apply_matrix_add algebra_simps)
 
 lemma Rep_scalar_mult[simp]: "Rep_matrix (scalar_mult y a) j i = y * (Rep_matrix a j i)" 
-by (simp add: scalar_mult_def)
+  by (simp add: scalar_mult_def)
 
 lemma scalar_mult_singleton[simp]: "scalar_mult y (singleton_matrix j i x) = singleton_matrix j i (y * x)"
-apply (subst Rep_matrix_inject[symmetric])
-apply (rule ext)+
-apply (auto)
-done
+  by (simp add: scalar_mult_def)
 
 lemma Rep_minus[simp]: "Rep_matrix (-(A::_::group_add)) x y = - (Rep_matrix A x y)"
-by (simp add: minus_matrix_def)
+  by (simp add: minus_matrix_def)
 
 lemma Rep_abs[simp]: "Rep_matrix \<bar>A::_::lattice_ab_group_add\<bar> x y = \<bar>Rep_matrix A x y\<bar>"
-by (simp add: abs_lattice sup_matrix_def)
+  by (simp add: abs_lattice sup_matrix_def)
 
 end
diff -r 17d8b3f6d744 -r c8bcb14fcfa8 src/HOL/Matrix_LP/SparseMatrix.thy
--- a/src/HOL/Matrix_LP/SparseMatrix.thy	Wed Aug 21 14:09:44 2024 +0100
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Thu Aug 22 22:26:28 2024 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory SparseMatrix
-imports Matrix
+  imports Matrix 
 begin
 
 type_synonym 'a spvec = "(nat * 'a) list"
@@ -30,75 +30,70 @@
 
 lemma sparse_row_vector_cons[simp]:
   "sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
-  apply (induct arr)
-  apply (auto simp add: sparse_row_vector_def)
-  apply (simp add: foldl_distrstart [of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
-  done
+  by (induct arr) (auto simp: foldl_distrstart sparse_row_vector_def)
 
 lemma sparse_row_vector_append[simp]:
   "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
   by (induct a) auto
 
-lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
-  apply (induct x)
-  apply (simp_all add: add_nrows)
-  done
+lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) \<le> (Suc 0)"
+  by (induct x) (auto simp: add_nrows)
 
 lemma sparse_row_matrix_cons: "sparse_row_matrix (a#arr) = ((move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)) + sparse_row_matrix arr"
-  apply (induct arr)
-  apply (auto simp add: sparse_row_matrix_def)
-  apply (simp add: foldl_distrstart[of "\<lambda>m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)" 
-    "% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"])
-  done
+  by (induct arr) (auto simp: foldl_distrstart sparse_row_matrix_def)
 
 lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)"
-  apply (induct arr)
-  apply (auto simp add: sparse_row_matrix_cons)
-  done
+  by (induct arr) (auto simp: sparse_row_matrix_cons)
 
-primrec sorted_spvec :: "'a spvec \<Rightarrow> bool"
+fun sorted_spvec :: "'a spvec \<Rightarrow> bool"
 where
   "sorted_spvec [] = True"
-| sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
+| sorted_spvec_step1: "sorted_spvec [a] = True" 
+| sorted_spvec_step: "sorted_spvec ((m,x)#(n,y)#bs) =  ((m < n) \<and> (sorted_spvec ((n,y)#bs)))" 
 
 primrec sorted_spmat :: "'a spmat \<Rightarrow> bool"
 where
   "sorted_spmat [] = True"
-| "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
+| "sorted_spmat (a#as) = ((sorted_spvec (snd a)) \<and> (sorted_spmat as))"
 
 declare sorted_spvec.simps [simp del]
 
 lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True"
-by (simp add: sorted_spvec.simps)
+  by (simp add: sorted_spvec.simps)
 
 lemma sorted_spvec_cons1: "sorted_spvec (a#as) \<Longrightarrow> sorted_spvec as"
-apply (induct as)
-apply (auto simp add: sorted_spvec.simps)
-done
+  using sorted_spvec.elims(2) sorted_spvec_empty by blast
 
 lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \<Longrightarrow> sorted_spvec (a#t)"
-apply (induct t)
-apply (auto simp add: sorted_spvec.simps)
-done
+  by (smt (verit, del_insts) sorted_spvec_step order.strict_trans list.inject sorted_spvec.elims(3) surj_pair)
 
 lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \<Longrightarrow> fst a < fst b"
-apply (auto simp add: sorted_spvec.simps)
-done
+  by (metis sorted_spvec_step prod.collapse)
 
-lemma sorted_sparse_row_vector_zero[rule_format]: "m <= n \<Longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_vector arr) j m = 0"
-apply (induct arr)
-apply (auto)
-apply (frule sorted_spvec_cons2,simp)+
-apply (frule sorted_spvec_cons3, simp)
-done
+lemma sorted_sparse_row_vector_zero: 
+  assumes "m \<le> n"
+  shows "sorted_spvec ((n,a)#arr) \<Longrightarrow> Rep_matrix (sparse_row_vector arr) j m = 0"
+proof (induct arr)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a arr)
+  with assms show ?case
+    by (auto dest: sorted_spvec_cons2 sorted_spvec_cons3)
+qed
 
-lemma sorted_sparse_row_matrix_zero[rule_format]: "m <= n \<Longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_matrix arr) m j = 0"
-  apply (induct arr)
-  apply (auto)
-  apply (frule sorted_spvec_cons2, simp)
-  apply (frule sorted_spvec_cons3, simp)
-  apply (simp add: sparse_row_matrix_cons)
-  done
+lemma sorted_sparse_row_matrix_zero[rule_format]: 
+  assumes "m \<le> n"
+  shows "sorted_spvec ((n,a)#arr) \<Longrightarrow> Rep_matrix (sparse_row_matrix arr) m j = 0"
+proof (induct arr)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a arr)
+  with assms show ?case
+    unfolding sparse_row_matrix_cons
+    by (auto dest: sorted_spvec_cons2 sorted_spvec_cons3)
+qed
 
 primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
 where
@@ -112,49 +107,45 @@
 
 lemma sparse_row_vector_minus: 
   "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
-  apply (induct v)
-  apply (simp_all add: sparse_row_vector_cons)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  done
-
-instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
-  apply standard
-  unfolding abs_matrix_def
-  apply rule
-  done
-  (*FIXME move*)
+proof (induct v)
+  case Nil
+  then show ?case
+    by auto
+next
+  case (Cons a v)
+  then have "singleton_matrix 0 (fst a) (- snd a) = - singleton_matrix 0 (fst a) (snd a)"
+    by (simp add: Rep_matrix_inject minus_matrix_def)
+  then show ?case
+    by (simp add: local.Cons)
+qed
 
 lemma sparse_row_vector_abs:
   "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = \<bar>sparse_row_vector v\<bar>"
-  apply (induct v)
-  apply simp_all
-  apply (frule_tac sorted_spvec_cons1, simp)
-  apply (simp only: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply auto
-  apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
-  apply (simp)
-  apply (rule sorted_sparse_row_vector_zero)
-  apply auto
-  done
+proof (induct v)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons ab v)
+  then have v: "sorted_spvec v"
+    using sorted_spvec_cons1 by blast
+  show ?case
+  proof (cases ab)
+    case (Pair a b)
+    then have 0: "Rep_matrix (sparse_row_vector v) 0 a = 0"
+      using Cons.prems sorted_sparse_row_vector_zero by blast
+    with v Cons show ?thesis
+      by (fastforce simp: Pair simp flip: Rep_matrix_inject)
+  qed
+qed
 
 lemma sorted_spvec_minus_spvec:
   "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
-  apply (induct v)
-  apply (simp)
-  apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+  by (induct v rule: sorted_spvec.induct) (auto simp: sorted_spvec_step1 sorted_spvec_step)
 
 lemma sorted_spvec_abs_spvec:
   "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
-  apply (induct v)
-  apply (simp)
-  apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+  by (induct v rule: sorted_spvec.induct) (auto simp: sorted_spvec_step1 sorted_spvec_step)
   
 definition "smult_spvec y = map (% a. (fst a, y * snd a))"  
 
@@ -178,68 +169,65 @@
   by (induct a) auto
 
 lemma addmult_spvec_empty2[simp]: "addmult_spvec y a [] = a"
-  by (induct a) auto
+  by simp
 
 lemma sparse_row_vector_map: "(\<forall>x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lattice_ring)) 0 = 0 \<Longrightarrow> 
   sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)"
-  apply (induct a)
-  apply (simp_all add: apply_matrix_add)
-  done
+  by (induct a) (simp_all add: apply_matrix_add)
 
 lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)"
-  apply (induct a)
-  apply (simp_all add: smult_spvec_cons scalar_mult_add)
-  done
+  by (induct a) (simp_all add: smult_spvec_cons scalar_mult_add)
 
 lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lattice_ring) a b) = 
   (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
-  apply (induct y a b rule: addmult_spvec.induct)
-  apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
-  done
+  by (induct y a b rule: addmult_spvec.induct)
+     (simp_all add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)
 
 lemma sorted_smult_spvec: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
-  apply (auto simp add: smult_spvec_def)
-  apply (induct a)
-  apply (auto simp add: sorted_spvec.simps split:list.split_asm)
-  done
+  by (induct a rule: sorted_spvec.induct) (auto simp: smult_spvec_def sorted_spvec_step1 sorted_spvec_step)
 
 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec y ((a, b) # arr) brr); aa < a; sorted_spvec ((a, b) # arr); 
   sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec y ((a, b) # arr) brr)"  
-  apply (induct brr)
-  apply (auto simp add: sorted_spvec.simps)
-  done
+  by (induct brr) (auto simp: sorted_spvec.simps)
 
 lemma sorted_spvec_addmult_spvec_helper2: 
  "\<lbrakk>sorted_spvec (addmult_spvec y arr ((aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
        \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec y arr ((aa, ba) # brr))"
-  apply (induct arr)
-  apply (auto simp add: smult_spvec_def sorted_spvec.simps)
-  done
+  by (induct arr) (auto simp: smult_spvec_def sorted_spvec.simps)
 
 lemma sorted_spvec_addmult_spvec_helper3[rule_format]:
-  "sorted_spvec (addmult_spvec y arr brr) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
-     \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec y arr brr))"
-  apply (induct y arr brr rule: addmult_spvec.induct)
-  apply (simp_all add: sorted_spvec.simps smult_spvec_def split:list.split)
-  done
+  "sorted_spvec (addmult_spvec y arr brr) \<Longrightarrow> 
+   sorted_spvec ((aa, b) # arr) \<Longrightarrow> 
+  sorted_spvec ((aa, ba) # brr) \<Longrightarrow>
+   sorted_spvec ((aa, b + y * ba) # (addmult_spvec y arr brr))"
+  by (smt (verit, ccfv_threshold) sorted_spvec_step addmult_spvec.simps(1) list.distinct(1) list.sel(3) sorted_spvec.elims(1) sorted_spvec_addmult_spvec_helper2)
 
 lemma sorted_addmult_spvec: "sorted_spvec a \<Longrightarrow> sorted_spvec b \<Longrightarrow> sorted_spvec (addmult_spvec y a b)"
-  apply (induct y a b rule: addmult_spvec.induct)
-  apply (simp_all add: sorted_smult_spvec)
-  apply (rule conjI, intro strip)
-  apply (case_tac "~(i < j)")
-  apply (simp_all)
-  apply (frule_tac as=brr in sorted_spvec_cons1)
-  apply (simp add: sorted_spvec_addmult_spvec_helper)
-  apply (intro strip | rule conjI)+
-  apply (frule_tac as=arr in sorted_spvec_cons1)
-  apply (simp add: sorted_spvec_addmult_spvec_helper2)
-  apply (intro strip)
-  apply (frule_tac as=arr in sorted_spvec_cons1)
-  apply (frule_tac as=brr in sorted_spvec_cons1)
-  apply (simp)
-  apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
-  done
+proof (induct y a b rule: addmult_spvec.induct)
+  case (1 y arr)
+  then show ?case
+    by simp
+next
+  case (2 y v va)
+  then show ?case 
+    by (simp add: sorted_smult_spvec)
+next
+  case (3 y i a arr j b brr)
+  show ?case 
+  proof (cases i j rule: linorder_cases)
+    case less
+    with 3 show ?thesis
+      by (simp add: sorted_spvec_addmult_spvec_helper2 sorted_spvec_cons1)
+  next
+    case equal
+    with 3 show ?thesis 
+      by (simp add: sorted_spvec_addmult_spvec_helper3 sorted_spvec_cons1)
+  next
+    case greater
+    with 3 show ?thesis 
+      by (simp add: sorted_spvec_addmult_spvec_helper sorted_spvec_cons1)
+  qed
+qed
 
 fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec"
 where
@@ -250,100 +238,85 @@
      else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr 
      else mult_spvec_spmat (addmult_spvec a c b) arr brr)"
 
-lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lattice_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> 
-  sparse_row_vector (mult_spvec_spmat c a B) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
+lemma sparse_row_mult_spvec_spmat: 
+  assumes "sorted_spvec (a::('a::lattice_ring) spvec)" "sorted_spvec B"
+  shows "sparse_row_vector (mult_spvec_spmat c a B) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
 proof -
-  have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith
+  have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 \<le> nat ((int b)-(int a))" by arith
   have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp
-  have max_helper: "!! a b. ~ (a <= max (Suc a) b) \<Longrightarrow> False"
-    by arith
   {
     fix a 
-    fix v
-    assume a:"a < nrows(sparse_row_vector v)"
-    have b:"nrows(sparse_row_vector v) <= 1" by simp
-    note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b]   
-    then have "a = 0" by simp
+    fix v :: "(nat \<times> 'a) list"
+    assume a: "a < nrows(sparse_row_vector v)"
+    have "nrows(sparse_row_vector v) \<le> 1" by simp
+    then have "a = 0"
+      using a dual_order.strict_trans1 by blast
   }
   note nrows_helper = this
   show ?thesis
-    apply (induct c a B rule: mult_spvec_spmat.induct)
-    apply simp+
-    apply (rule conjI)
-    apply (intro strip)
-    apply (frule_tac as=brr in sorted_spvec_cons1)
-    apply (simp add: algebra_simps sparse_row_matrix_cons)
-    apply (simplesubst Rep_matrix_zero_imp_mult_zero) 
-    apply (simp)
-    apply (rule disjI2)
-    apply (intro strip)
-    apply (subst nrows)
-    apply (rule  order_trans[of _ 1])
-    apply (simp add: comp_1)+
-    apply (subst Rep_matrix_zero_imp_mult_zero)
-    apply (intro strip)
-    apply (case_tac "k <= j")
-    apply (rule_tac m1 = k and n1 = i and a1 = a in ssubst[OF sorted_sparse_row_vector_zero])
-    apply (simp_all)
-    apply (rule disjI2)
-    apply (rule nrows)
-    apply (rule order_trans[of _ 1])
-    apply (simp_all add: comp_1)
-    
-    apply (intro strip | rule conjI)+
-    apply (frule_tac as=arr in sorted_spvec_cons1)
-    apply (simp add: algebra_simps)
-    apply (subst Rep_matrix_zero_imp_mult_zero)
-    apply (simp)
-    apply (rule disjI2)
-    apply (intro strip)
-    apply (simp add: sparse_row_matrix_cons)
-    apply (case_tac "i <= j")  
-    apply (erule sorted_sparse_row_matrix_zero)  
-    apply (simp_all)
-    apply (intro strip)
-    apply (case_tac "i=j")
-    apply (simp_all)
-    apply (frule_tac as=arr in sorted_spvec_cons1)
-    apply (frule_tac as=brr in sorted_spvec_cons1)
-    apply (simp add: sparse_row_matrix_cons algebra_simps sparse_row_vector_addmult_spvec)
-    apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
-    apply (auto)
-    apply (rule sorted_sparse_row_matrix_zero)
-    apply (simp_all)
-    apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
-    apply (auto)
-    apply (rule_tac m=k and n = j and a = a and arr=arr in sorted_sparse_row_vector_zero)
-    apply (simp_all)
-    apply (drule nrows_notzero)
-    apply (drule nrows_helper)
-    apply (arith)
-    
-    apply (subst Rep_matrix_inject[symmetric])
-    apply (rule ext)+
-    apply (simp)
-    apply (subst Rep_matrix_mult)
-    apply (rule_tac j1=j in ssubst[OF foldseq_almostzero])
-    apply (simp_all)
-    apply (intro strip, rule conjI)
-    apply (intro strip)
-    apply (drule_tac max_helper)
-    apply (simp)
-    apply (auto)
-    apply (rule zero_imp_mult_zero)
-    apply (rule disjI2)
-    apply (rule nrows)
-    apply (rule order_trans[of _ 1])
-    apply (simp)
-    apply (simp)
-    done
+    using assms
+  proof (induct c a B rule: mult_spvec_spmat.induct)
+    case (1 c brr)
+    then show ?case
+      by simp
+  next
+    case (2 c v va)
+    then show ?case
+      by simp
+  next
+    case (3 c i a arr j b brr)
+    then have abrr: "sorted_spvec arr" "sorted_spvec brr"
+      using sorted_spvec_cons1 by blast+
+    have "\<And>m n. \<lbrakk>a \<noteq> 0; 0 < m\<rbrakk>
+           \<Longrightarrow> a * Rep_matrix (sparse_row_vector b) m n = 0"
+      by (metis mult_zero_right neq0_conv nrows_helper nrows_notzero)
+    then have \<dagger>: "scalar_mult a (sparse_row_vector b) =
+            singleton_matrix 0 j a * move_matrix (sparse_row_vector b) (int j) 0"
+      apply (intro matrix_eqI)
+      apply (simp)
+      apply (subst Rep_matrix_mult)
+      apply (subst foldseq_almostzero, auto)
+      done
+    show ?case
+    proof (cases i j rule: linorder_cases)
+      case less
+      with 3 abrr \<dagger> show ?thesis
+        apply (simp add: algebra_simps sparse_row_matrix_cons Rep_matrix_zero_imp_mult_zero)
+        by (metis Rep_matrix_zero_imp_mult_zero Rep_singleton_matrix less_imp_le_nat sorted_sparse_row_matrix_zero)
+    next
+      case equal
+      with 3 abrr \<dagger> show ?thesis
+        apply (simp add: sparse_row_matrix_cons algebra_simps sparse_row_vector_addmult_spvec)
+        apply (subst Rep_matrix_zero_imp_mult_zero)
+        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: )
+        done
+    next
+      case greater
+      have "Rep_matrix (sparse_row_vector arr) j' k = 0 \<or>
+           Rep_matrix (move_matrix (sparse_row_vector b) (int j) 0) k
+            i' = 0"
+        if "sorted_spvec ((i, a) # arr)" for j' i' k
+      proof (cases "k \<le> j")
+        case True
+        with greater that show ?thesis
+          by (meson order.trans nat_less_le sorted_sparse_row_vector_zero)
+      qed (use nrows_helper nrows_notzero in force)
+      then have "sparse_row_vector arr * move_matrix (sparse_row_vector b) (int j) 0 = 0"
+        using greater 3 
+        by (simp add: Rep_matrix_zero_imp_mult_zero)
+      with greater 3 abrr show ?thesis
+        apply (simp add: algebra_simps sparse_row_matrix_cons)
+        by (metis Rep_matrix_zero_imp_mult_zero Rep_move_matrix Rep_singleton_matrix comp_1 nrows_le nrows_spvec)
+    qed
+  qed
 qed
 
-lemma sorted_mult_spvec_spmat[rule_format]: 
-  "sorted_spvec (c::('a::lattice_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat c a B)"
-  apply (induct c a B rule: mult_spvec_spmat.induct)
-  apply (simp_all add: sorted_addmult_spvec)
-  done
+lemma sorted_mult_spvec_spmat: 
+  "sorted_spvec (c::('a::lattice_ring) spvec) \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spvec (mult_spvec_spmat c a B)"
+  by (induct c a B rule: mult_spvec_spmat.induct) (simp_all add: sorted_addmult_spvec)
 
 primrec mult_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
 where
@@ -353,24 +326,16 @@
 lemma sparse_row_mult_spmat: 
   "sorted_spmat A \<Longrightarrow> sorted_spvec B \<Longrightarrow>
    sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
-  apply (induct A)
-  apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat algebra_simps move_matrix_mult)
-  done
+  by (induct A) (auto simp: sparse_row_matrix_cons sparse_row_mult_spvec_spmat algebra_simps move_matrix_mult)
 
-lemma sorted_spvec_mult_spmat[rule_format]:
-  "sorted_spvec (A::('a::lattice_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)"
-  apply (induct A)
-  apply (auto)
-  apply (drule sorted_spvec_cons1, simp)
-  apply (case_tac A)
-  apply (auto simp add: sorted_spvec.simps)
-  done
+lemma sorted_spvec_mult_spmat:
+  fixes A :: "('a::lattice_ring) spmat"
+  shows "sorted_spvec A \<Longrightarrow> sorted_spvec (mult_spmat A B)"
+by (induct A rule: sorted_spvec.induct) (auto simp: sorted_spvec.simps)
 
 lemma sorted_spmat_mult_spmat:
   "sorted_spmat (B::('a::lattice_ring) spmat) \<Longrightarrow> sorted_spmat (mult_spmat A B)"
-  apply (induct A)
-  apply (auto simp add: sorted_mult_spvec_spmat) 
-  done
+  by (induct A) (auto simp: sorted_mult_spvec_spmat) 
 
 
 fun add_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
@@ -384,12 +349,10 @@
      else (i, a+b) # add_spvec arr brr)"
 
 lemma add_spvec_empty1[simp]: "add_spvec [] a = a"
-by (cases a, auto)
+  by (cases a, auto)
 
 lemma sparse_row_vector_add: "sparse_row_vector (add_spvec a b) = (sparse_row_vector a) + (sparse_row_vector b)"
-  apply (induct a b rule: add_spvec.induct)
-  apply (simp_all add: singleton_matrix_add)
-  done
+  by (induct a b rule: add_spvec.induct) (simp_all add: singleton_matrix_add)
 
 fun add_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
 where
@@ -408,127 +371,67 @@
 by(cases as) auto
 
 lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat A B) = (sparse_row_matrix A) + (sparse_row_matrix B)"
-  apply (induct A B rule: add_spmat.induct)
-  apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
-  done
+  by (induct A B rule: add_spmat.induct) (auto simp: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
 
 lemmas [code] = sparse_row_add_spmat [symmetric]
 lemmas [code] = sparse_row_vector_add [symmetric]
 
 lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
-  proof - 
-    have "(\<forall>x ab a. x = (a,b)#arr \<longrightarrow> add_spvec x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
-      by (induct brr rule: add_spvec.induct) (auto split:if_splits)
-    then show ?thesis
-      by (case_tac brr, auto)
-  qed
+proof - 
+  have "(\<forall>x ab a. x = (a,b)#arr \<longrightarrow> add_spvec x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
+    by (induct brr rule: add_spvec.induct) (auto split:if_splits)
+  then show ?thesis
+    by (case_tac brr, auto)
+qed
 
-lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
-  proof - 
-    have "(\<forall>x ab a. x = (a,b)#arr \<longrightarrow> add_spmat x brr = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
-      by (rule add_spmat.induct) (auto split:if_splits)
-    then show ?thesis
-      by (case_tac brr, auto)
-  qed
+lemma sorted_add_spmat_helper1[rule_format]:
+  "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
+  by (smt (verit) add_spmat.elims fst_conv list.distinct(1) list.sel(1))
 
 lemma sorted_add_spvec_helper: "add_spvec arr brr = (ab, bb) # list \<Longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
-  apply (induct arr brr rule: add_spvec.induct)
-  apply (auto split:if_splits)
-  done
+  by (induct arr brr rule: add_spvec.induct) (auto split:if_splits)
 
 lemma sorted_add_spmat_helper: "add_spmat arr brr = (ab, bb) # list \<Longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
-  apply (induct arr brr rule: add_spmat.induct)
-  apply (auto split:if_splits)
-  done
+  by (induct arr brr rule: add_spmat.induct) (auto split:if_splits)
 
 lemma add_spvec_commute: "add_spvec a b = add_spvec b a"
 by (induct a b rule: add_spvec.induct) auto
 
 lemma add_spmat_commute: "add_spmat a b = add_spmat b a"
-  apply (induct a b rule: add_spmat.induct)
-  apply (simp_all add: add_spvec_commute)
-  done
+  by (induct a b rule: add_spmat.induct) (simp_all add: add_spvec_commute)
   
 lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
-  apply (drule sorted_add_spvec_helper1)
-  apply (auto)
-  apply (case_tac brr)
-  apply (simp_all)
-  apply (drule_tac sorted_spvec_cons3)
-  apply (simp)
-  done
+  by (smt (verit, best) add_spvec.elims fst_conv list.sel(1) sorted_spvec_cons3)
 
 lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr) brr = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
-  apply (drule sorted_add_spmat_helper1)
-  apply (auto)
-  apply (case_tac brr)
-  apply (simp_all)
-  apply (drule_tac sorted_spvec_cons3)
-  apply (simp)
-  done
+  by (metis (no_types, opaque_lifting) add_spmat.simps(1) list.sel(1) neq_Nil_conv sorted_add_spmat_helper sorted_spvec_cons3)
+
+lemma sorted_spvec_add_spvec: "sorted_spvec a \<Longrightarrow> sorted_spvec b \<Longrightarrow> sorted_spvec (add_spvec a b)"
+proof (induct a b rule: add_spvec.induct)
+  case (3 i a arr j b brr)
+  then have "sorted_spvec arr" "sorted_spvec brr"
+    using sorted_spvec_cons1 by blast+
+  with 3 show ?case
+    apply simp
+    by (smt (verit, ccfv_SIG) add_spvec.simps(2) list.sel(3) sorted_add_spvec_helper sorted_spvec.elims(1))
+qed auto
 
-lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec a b)"
-  apply (induct a b rule: add_spvec.induct)
-  apply (simp_all)
-  apply (rule conjI)
-  apply (clarsimp)
-  apply (frule_tac as=brr in sorted_spvec_cons1)
-  apply (simp)
-  apply (subst sorted_spvec_step)
-  apply (clarsimp simp: sorted_add_spvec_helper2 split: list.split)
-  apply (clarify)
-  apply (rule conjI)
-  apply (clarify)
-  apply (frule_tac as=arr in sorted_spvec_cons1, simp)
-  apply (subst sorted_spvec_step)
-  apply (clarsimp simp: sorted_add_spvec_helper2 add_spvec_commute split: list.split)
-  apply (clarify)
-  apply (frule_tac as=arr in sorted_spvec_cons1)
-  apply (frule_tac as=brr in sorted_spvec_cons1)
-  apply (simp)
-  apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarsimp)
-  apply (drule_tac sorted_add_spvec_helper)
-  apply (auto simp: neq_Nil_conv)
-  apply (drule sorted_spvec_cons3)
-  apply (simp)
-  apply (drule sorted_spvec_cons3)
-  apply (simp)
-  done
-
-lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat A B)"
-  apply (induct A B rule: add_spmat.induct)
-  apply (simp_all)
-  apply (rule conjI)
-  apply (intro strip)
-  apply (simp)
-  apply (frule_tac as=bs in sorted_spvec_cons1)
-  apply (simp)
-  apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarify, simp)
-  apply (simp add: sorted_add_spmat_helper2)
-  apply (clarify)
-  apply (rule conjI)
-  apply (clarify)
-  apply (frule_tac as=as in sorted_spvec_cons1, simp)
-  apply (subst sorted_spvec_step)
-  apply (clarsimp simp: sorted_add_spmat_helper2 add_spmat_commute split: list.split)
-  apply (clarsimp)
-  apply (frule_tac as=as in sorted_spvec_cons1)
-  apply (frule_tac as=bs in sorted_spvec_cons1)
-  apply (simp)
-  apply (subst sorted_spvec_step)
-  apply (simp split: list.split)
-  apply (clarify, simp)
-  apply (drule_tac sorted_add_spmat_helper)
-  apply (auto simp:neq_Nil_conv)
-  apply (drule sorted_spvec_cons3)
-  apply (simp)
-  apply (drule sorted_spvec_cons3)
-  apply (simp)
-  done
+lemma sorted_spvec_add_spmat:
+  "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (add_spmat A B)"
+proof (induct A B rule: add_spmat.induct)
+  case (1 bs)
+  then show ?case by auto
+next
+  case (2 v va)
+  then show ?case by auto
+next
+  case (3 i a as j b bs)
+  then have "sorted_spvec as" "sorted_spvec bs"
+    using sorted_spvec_cons1 by blast+
+  with 3 show ?case
+    apply simp
+    by (smt (verit) Pair_inject add_spmat.elims list.discI list.inject sorted_spvec.elims(1))
+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)
@@ -539,12 +442,12 @@
 where
 (* "measure (% (a,b). (length a) + (length b))" *)
   "le_spvec [] [] = True"
-| "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])"
-| "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)"
+| "le_spvec ((_,a)#as) [] = (a \<le> 0 & le_spvec as [])"
+| "le_spvec [] ((_,b)#bs) = (0 \<le> b & le_spvec [] bs)"
 | "le_spvec ((i,a)#as) ((j,b)#bs) = (
-    if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
-    else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
-    else a <= b & le_spvec as bs)"
+    if (i < j) then a \<le> 0 & le_spvec as ((j,b)#bs)
+    else if (j < i) then 0 \<le> b & le_spvec ((i,a)#as) bs
+    else a \<le> b & le_spvec as bs)"
 
 fun le_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool"
 where
@@ -571,7 +474,7 @@
 
 
 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 <= C + D) = (A <= C & B <= (D::('a::lattice_ab_group_add) matrix))"
+  (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)
@@ -598,25 +501,25 @@
 by (simp add: disj_matrices_def)
 
 lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A"
-by (auto simp add: disj_matrices_def)
+by (auto simp: disj_matrices_def)
 
 lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
-  (A + B <= 0) = (A <= 0 & (B::('a::lattice_ab_group_add) matrix) <= 0)"
+  (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])
  
 lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
-  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lattice_ab_group_add) matrix))"
+  (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])
 
 lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
-  (A <= B + C) = (A <= C & 0 <= (B::('a::lattice_ab_group_add) matrix))"
-by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
+  (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])
 
 lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
-  (B + A <= C) = (A <= C &  (B::('a::lattice_ab_group_add) matrix) <= 0)"
-by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
+  (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)
 
-lemma disj_sparse_row_singleton: "i <= j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)"
+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)
@@ -642,11 +545,11 @@
   by (simp add: disj_matrices_x_add disj_matrices_commute)
 
 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 add: disj_matrices_def)
+  by (auto simp: disj_matrices_def)
 
 lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: 
-  "j <= 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 add: disj_matrices_def)
+  "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")
@@ -663,11 +566,11 @@
 
 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 add: disj_matrices_def)
+  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 <= sparse_row_vector b)"
+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)
@@ -689,24 +592,24 @@
   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 <= 0)"
+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 add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
+  apply (auto simp: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
   done
 
-lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec [] b = (0 <= sparse_row_vector b))"
+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 add: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
+  apply (auto simp: disj_matrices_commute disj_sparse_row_singleton[OF order_refl] sorted_spvec_cons1)
   done
 
 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> 
-  le_spmat A B = (sparse_row_matrix A <= sparse_row_matrix B)"
+  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)+ 
@@ -748,66 +651,58 @@
 
 lemma sparse_row_matrix_minus:
   "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
-  apply (induct A)
-  apply (simp_all add: sparse_row_vector_minus sparse_row_matrix_cons)
-  apply (subst Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  done
+proof (induct A)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a A)
+  then show ?case
+    by (simp add: sparse_row_vector_minus sparse_row_matrix_cons matrix_eqI)
+qed
 
-lemma Rep_sparse_row_vector_zero: "x \<noteq> 0 \<Longrightarrow> Rep_matrix (sparse_row_vector v) x y = 0"
-proof -
-  assume x:"x \<noteq> 0"
-  have r:"nrows (sparse_row_vector v) <= Suc 0" by (rule nrows_spvec)
-  show ?thesis
-    apply (rule nrows)
-    apply (subgoal_tac "Suc 0 <= x")
-    apply (insert r)
-    apply (simp only:)
-    apply (insert x)
-    apply arith
-    done
-qed
+lemma Rep_sparse_row_vector_zero:
+  assumes "x \<noteq> 0"
+    shows "Rep_matrix (sparse_row_vector v) x y = 0"
+  by (metis Suc_leI assms le0 le_eq_less_or_eq nrows_le nrows_spvec)
     
 lemma sparse_row_matrix_abs:
   "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = \<bar>sparse_row_matrix A\<bar>"
-  apply (induct A)
-  apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
-  apply (frule_tac sorted_spvec_cons1, simp)
-  apply (simplesubst Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply auto
-  apply (case_tac "x=a")
-  apply (simp)
-  apply (simplesubst sorted_sparse_row_matrix_zero)
-  apply auto
-  apply (simplesubst Rep_sparse_row_vector_zero)
-  apply simp_all
-  done
+proof (induct A)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons ab A)
+  then have A: "sorted_spvec A"
+    using sorted_spvec_cons1 by blast
+  show ?case 
+  proof (cases ab)
+    case (Pair a b)
+    show ?thesis
+      unfolding Pair
+    proof (intro matrix_eqI)
+      fix m n
+      show "Rep_matrix (sparse_row_matrix (abs_spmat ((a,b) # A))) m n 
+          = Rep_matrix \<bar>sparse_row_matrix ((a,b) # A)\<bar> m n"
+        using Cons Pair A 
+        apply (simp add: sparse_row_vector_abs sparse_row_matrix_cons)
+        apply (cases "m=a")
+        using sorted_sparse_row_matrix_zero apply fastforce
+        by (simp add: Rep_sparse_row_vector_zero)
+    qed
+  qed
+qed
 
 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"
-  apply (induct A)
-  apply (simp)
-  apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done 
+by (induct A rule: sorted_spvec.induct) (auto simp: sorted_spvec.simps)
 
 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" 
-  apply (induct A)
-  apply (simp)
-  apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+  by (induct A rule: sorted_spvec.induct) (auto simp: sorted_spvec.simps)
 
 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
-  apply (induct A)
-  apply (simp_all add: sorted_spvec_minus_spvec)
-  done
+  by (induct A) (simp_all add: sorted_spvec_minus_spvec)
 
 lemma sorted_spmat_abs_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (abs_spmat A)"
-  apply (induct A)
-  apply (simp_all add: sorted_spvec_abs_spvec)
-  done
+  by (induct A) (simp_all add: sorted_spvec_abs_spvec)
 
 definition diff_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   where "diff_spmat A B = add_spmat A (minus_spmat B)"
@@ -872,148 +767,120 @@
 
 lemma pprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
   apply (simp add: pprt_def sup_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  apply (case_tac "Rep_matrix A x xa \<noteq> 0")
-  apply (simp_all add: disj_matrices_contr1)
-  done
+  apply (intro matrix_eqI)
+  by (smt (verit, del_insts) Rep_combine_matrix Rep_zero_matrix_def add.commute comm_monoid_add_class.add_0 disj_matrices_def plus_matrix_def sup.idem)
 
 lemma nprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
-  apply (simp add: nprt_def inf_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  apply (case_tac "Rep_matrix A x xa \<noteq> 0")
-  apply (simp_all add: disj_matrices_contr1)
-  done
+  unfolding nprt_def inf_matrix_def
+  apply (intro matrix_eqI)
+  by (smt (verit, ccfv_threshold) Rep_combine_matrix Rep_matrix_add add.commute add_cancel_right_right add_eq_inf_sup disj_matrices_contr2 sup.idem)
 
-lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lattice_ring)) = singleton_matrix j i (pprt x)"
-  apply (simp add: pprt_def sup_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  done
+lemma pprt_singleton[simp]: 
+  fixes x:: "_::lattice_ring"
+  shows "pprt (singleton_matrix j i x) = singleton_matrix j i (pprt x)"
+  unfolding pprt_def sup_matrix_def
+  by (simp add: matrix_eqI)
 
-lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lattice_ring)) = singleton_matrix j i (nprt x)"
-  apply (simp add: nprt_def inf_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply simp
-  done
+lemma nprt_singleton[simp]:
+  fixes x:: "_::lattice_ring"
+  shows "nprt (singleton_matrix j i x) = singleton_matrix j i (nprt x)"
+  by (metis add_left_imp_eq pprt_singleton prts singleton_matrix_add)
 
-lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
+lemma sparse_row_vector_pprt:
+  fixes v:: "_::lattice_ring spvec"
+  shows "sorted_spvec v \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
+proof (induct v rule: sorted_spvec.induct)
+  case (3 m x n y bs)
+  then show ?case
+    apply (simp add: )
+    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)
+qed auto
 
-lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
-  apply (induct v)
-  apply (simp_all)
-  apply (frule sorted_spvec_cons1, auto)
-  apply (subst pprt_add)
-  apply (subst disj_matrices_commute)
-  apply (rule disj_sparse_row_singleton)
-  apply auto
-  done
-
-lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
-  apply (induct v)
-  apply (simp_all)
-  apply (frule sorted_spvec_cons1, auto)
-  apply (subst nprt_add)
-  apply (subst disj_matrices_commute)
-  apply (rule disj_sparse_row_singleton)
-  apply auto
-  done
+lemma sparse_row_vector_nprt:
+  fixes v:: "_::lattice_ring spvec"
+  shows "sorted_spvec v \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
+proof (induct v rule: sorted_spvec.induct)
+  case (3 m x n y bs)
+  then show ?case
+    apply (simp add: )
+    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
+qed auto
   
   
 lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lattice_ring) matrix) j i) = move_matrix (pprt A) j i"
-  apply (simp add: pprt_def)
-  apply (simp add: sup_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply (simp)
-  done
+  by (simp add: pprt_def sup_matrix_def matrix_eqI)
 
 lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lattice_ring) matrix) j i) = move_matrix (nprt A) j i"
-  apply (simp add: nprt_def)
-  apply (simp add: inf_matrix_def)
-  apply (simp add: Rep_matrix_inject[symmetric])
-  apply (rule ext)+
-  apply (simp)
-  done
+  by (simp add: nprt_def inf_matrix_def matrix_eqI)
 
-lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lattice_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
-  apply (induct m)
-  apply simp
-  apply simp
-  apply (frule sorted_spvec_cons1)
-  apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
-  apply (subst pprt_add)
-  apply (subst disj_matrices_commute)
-  apply (rule disj_move_sparse_vec_mat)
-  apply auto
-  apply (simp add: sorted_spvec.simps)
-  apply (simp split: list.split)
-  apply auto
-  apply (simp add: pprt_move_matrix)
-  done
+lemma sparse_row_matrix_pprt: 
+  fixes m:: "'a::lattice_ring spmat"
+  shows "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
+proof (induct m rule: sorted_spvec.induct)
+  case (2 a)
+  then show ?case
+    by (simp add: pprt_move_matrix sparse_row_matrix_cons sparse_row_vector_pprt)
+next
+  case (3 m x n y bs)
+  then show ?case 
+    apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
+    apply (subst pprt_add)
+     apply (subst disj_matrices_commute)
+     apply (metis disj_move_sparse_vec_mat eq_imp_le fst_conv prod.sel(2) sparse_row_matrix_cons)
+    apply (simp add: sorted_spvec.simps pprt_move_matrix)
+    done
+qed auto
 
-lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lattice_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
-  apply (induct m)
-  apply simp
-  apply simp
-  apply (frule sorted_spvec_cons1)
-  apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
-  apply (subst nprt_add)
-  apply (subst disj_matrices_commute)
-  apply (rule disj_move_sparse_vec_mat)
-  apply auto
-  apply (simp add: sorted_spvec.simps)
-  apply (simp split: list.split)
-  apply auto
-  apply (simp add: nprt_move_matrix)
-  done
+lemma sparse_row_matrix_nprt:
+  fixes m:: "'a::lattice_ring spmat"
+  shows "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
+proof (induct m rule: sorted_spvec.induct)
+  case (2 a)
+  then show ?case
+    by (simp add: nprt_move_matrix sparse_row_matrix_cons sparse_row_vector_nprt)
+next
+  case (3 m x n y bs)
+  then show ?case
+    apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
+    apply (subst nprt_add)
+     apply (subst disj_matrices_commute)
+     apply (metis disj_move_sparse_vec_mat fst_conv nle_le prod.sel(2) sparse_row_matrix_cons)
+    apply (simp add: sorted_spvec.simps nprt_move_matrix)
+    done
+qed auto
 
 lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)"
-  apply (induct v)
-  apply (simp)
-  apply (frule sorted_spvec_cons1)
-  apply simp
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+proof (induct v rule: sorted_spvec.induct)
+  case 1
+  then show ?case by auto
+next
+  case (2 a)
+  then show ?case 
+    by (simp add: sorted_spvec_step1)
+next
+  case (3 m x n y bs)
+  then show ?case
+    by (simp add: sorted_spvec_step)
+qed
 
 lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
-  apply (induct v)
-  apply (simp)
-  apply (frule sorted_spvec_cons1)
-  apply simp
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+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)"
-  apply (induct m)
-  apply (simp)
-  apply (frule sorted_spvec_cons1)
-  apply simp
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+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)"
-  apply (induct m)
-  apply (simp)
-  apply (frule sorted_spvec_cons1)
-  apply simp
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
+by (induct m rule: sorted_spvec.induct) (simp_all add: sorted_spvec.simps split:list.split_asm)
 
 lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)"
-  apply (induct m)
-  apply (simp_all add: sorted_pprt_spvec)
-  done
+  by (induct m) (simp_all add: sorted_pprt_spvec)
 
 lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)"
-  apply (induct m)
-  apply (simp_all add: sorted_nprt_spvec)
-  done
+  by (induct m) (simp_all add: sorted_nprt_spvec)
 
 definition mult_est_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
   "mult_est_spmat r1 r2 s1 s2 =
@@ -1056,10 +923,10 @@
   "sorted_spvec r"
   "le_spmat ([], y)"
   "A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
-  "sparse_row_matrix A1 <= A"
-  "A <= sparse_row_matrix A2"
-  "sparse_row_matrix c1 <= c"
-  "c <= sparse_row_matrix c2"
+  "sparse_row_matrix A1 \<le> A"
+  "A \<le> sparse_row_matrix A2"
+  "sparse_row_matrix c1 \<le> c"
+  "c \<le> sparse_row_matrix c2"
   "\<bar>x\<bar> \<le> sparse_row_matrix r"
   shows
   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1),