# HG changeset patch
# User wenzelm
# Date 1082746166 -7200
# Node ID d2c6a0f030ab7d5f5fdac87f20242389de84b65b
# Parent  9ead82084de823448a0a22099b6d18da0709196a
proper document setup;

diff -r 9ead82084de8 -r d2c6a0f030ab src/HOL/Matrix/LinProg.thy
--- a/src/HOL/Matrix/LinProg.thy	Fri Apr 23 20:48:28 2004 +0200
+++ b/src/HOL/Matrix/LinProg.thy	Fri Apr 23 20:49:26 2004 +0200
@@ -11,9 +11,9 @@
   fmuladdprops:
   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
   "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
-  "! a. fmul 0 a = 0"  
+  "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
-  "fadd 0 0 = 0" 
+  "fadd 0 0 = 0"
   "associative fadd"
   "commutative fadd"
   "associative fmul"
@@ -23,7 +23,7 @@
   "mult_matrix fmul fadd y A = c"
   "0 <= y"
   shows
-  "combine_matrix fadd (mult_matrix fmul fadd c x) (mult_matrix fmul fadd (mult_matrix fmul fadd y dA) x) 
+  "combine_matrix fadd (mult_matrix fmul fadd c x) (mult_matrix fmul fadd (mult_matrix fmul fadd y dA) x)
   <= mult_matrix fmul fadd y b"
 proof -
   let ?mul = "mult_matrix fmul fadd"
@@ -32,7 +32,7 @@
   have a: "?t1 <= ?mul y b" by (rule le_left_mult, simp_all!)
   have b: "?t1 = ?mul (?mul y (?add A dA)) x" by (simp! add: mult_matrix_assoc_simple[THEN sym])
   have assoc: "associative ?add" by (simp! add: combine_matrix_assoc)
-  have r_distr: "r_distributive ?mul ?add" 
+  have r_distr: "r_distributive ?mul ?add"
     apply (rule r_distributive_matrix)
     by (simp! add: distributive_def)+
   have l_distr: "l_distributive ?mul ?add"
@@ -73,12 +73,8 @@
   "c * x  <= y * b"
 proof -
   have a:"(A + 0) * x <= b" by (simp!)
-  have b:"c * x + (y*0)*x <= y * b" by (rule linprog_by_duality_approx, simp_all!) 
+  have b:"c * x + (y*0)*x <= y * b" by (rule linprog_by_duality_approx, simp_all!)
   show "c * x <= y*b" by (insert b, simp)
 qed
 
 end
-
-
-  
-  
diff -r 9ead82084de8 -r d2c6a0f030ab src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Apr 23 20:48:28 2004 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Apr 23 20:49:26 2004 +0200
@@ -4,7 +4,7 @@
     License:    2004 Technische Universität München
 *)
 
-theory Matrix=MatrixGeneral:
+theory Matrix = MatrixGeneral:
 
 axclass almost_matrix_element < zero, plus, times
 matrix_add_assoc: "(a+b)+c = a + (b+c)"
@@ -77,8 +77,8 @@
   have mult_right_zero: "!! A. A * (0::('a::matrix_element) matrix) = 0" by (simp add: times_matrix_def)
   note l_distributive_matrix2 = l_distributive_matrix[simplified l_distributive_def matrix_left_distrib, THEN spec, THEN spec, THEN spec]
   {
-    fix A::"('a::matrix_element) matrix" 
-    fix B 
+    fix A::"('a::matrix_element) matrix"
+    fix B
     fix C
     have "(A + B) * C = A * C + B * C"
       apply (simp add: plus_matrix_def)
@@ -86,15 +86,15 @@
       apply (rule l_distributive_matrix2)
       apply (simp_all add: associative_def commutative_def l_distributive_def)
       apply (auto)
-      apply (simp_all add: matrix_add_assoc) 
+      apply (simp_all add: matrix_add_assoc)
       apply (simp_all add: matrix_add_commute)
       by (simp_all add: matrix_left_distrib)
   }
   note left_distrib = this
   note r_distributive_matrix2 = r_distributive_matrix[simplified r_distributive_def matrix_right_distrib, THEN spec, THEN spec, THEN spec]
   {
-    fix A::"('a::matrix_element) matrix" 
-    fix B 
+    fix A::"('a::matrix_element) matrix"
+    fix B
     fix C
     have "C * (A + B) = C * A + C * B"
       apply (simp add: plus_matrix_def)
@@ -102,7 +102,7 @@
       apply (rule r_distributive_matrix2)
       apply (simp_all add: associative_def commutative_def r_distributive_def)
       apply (auto)
-      apply (simp_all add: matrix_add_assoc) 
+      apply (simp_all add: matrix_add_assoc)
       apply (simp_all add: matrix_add_commute)
       by (simp_all add: matrix_right_distrib)
   }
@@ -175,12 +175,12 @@
 proof -
   assume p1:"a <= b"
   assume p2:"c <= d"
-  have "a+c <= b+c" by (rule pordered_add_right_mono) 
+  have "a+c <= b+c" by (rule pordered_add_right_mono)
   also have "\<dots> <= b+d" by (rule pordered_add_left_mono)
   ultimately show "a+c <= b+d" by simp
 qed
 
-instance matrix :: (pordered_matrix_element) pordered_matrix_element 
+instance matrix :: (pordered_matrix_element) pordered_matrix_element
 apply (intro_classes)
 apply (simp_all add: plus_matrix_def times_matrix_def)
 apply (rule le_combine_matrix)
@@ -246,9 +246,9 @@
 apply (simp_all)
 by (simp add: max_def nrows)
 
-constdefs 
+constdefs
   right_inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
-  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))" 
+  "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
   inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
 
@@ -256,28 +256,6 @@
 apply (insert ncols_mult[of A X], insert nrows_mult[of A X])
 by (simp add: right_inverse_matrix_def)
 
-(* to be continued \<dots> *)
+text {* to be continued \dots *}
 
 end
-
-
-
-
-
-
-
-
-
-
-  
-  
-
-
-
-
-
-
-
-
-
- 
diff -r 9ead82084de8 -r d2c6a0f030ab src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Fri Apr 23 20:48:28 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Fri Apr 23 20:49:26 2004 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Matrix/MatrixGeneral.thy
     ID:         $Id$
     Author:     Steven Obua
-    License:    2004 Technische UniversitÃ\<currency>t MÃ\<onequarter>nchen
+    License:    2004 Technische Universitaet Muenchen
 *)
 
 theory MatrixGeneral = Main:
@@ -10,7 +10,7 @@
 
 constdefs
   nonzero_positions :: "('a::zero) infmatrix \<Rightarrow> (nat*nat) set"
-  "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}"  
+  "nonzero_positions A == {pos. A (fst pos) (snd pos) ~= 0}"
 
 typedef 'a matrix = "{(f::(('a::zero) infmatrix)). finite (nonzero_positions f)}"
 apply (rule_tac x="(% j i. 0)" in exI)
@@ -19,36 +19,36 @@
 declare Rep_matrix_inverse[simp]
 
 lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
-apply (rule Abs_matrix_induct) 
+apply (rule Abs_matrix_induct)
 by (simp add: Abs_matrix_inverse matrix_def)
 
 constdefs
   nrows :: "('a::zero) matrix \<Rightarrow> nat"
   "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
   ncols :: "('a::zero) matrix \<Rightarrow> nat"
-  "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))" 
+  "ncols A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image snd) (nonzero_positions (Rep_matrix A))))"
 
-lemma nrows: 
-  assumes hyp: "nrows A \<le> m" 
+lemma nrows:
+  assumes hyp: "nrows A \<le> m"
   shows "(Rep_matrix A m n) = 0" (is ?concl)
 proof cases
-  assume "nonzero_positions(Rep_matrix A) = {}" 
+  assume "nonzero_positions(Rep_matrix A) = {}"
   then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
 next
   assume a: "nonzero_positions(Rep_matrix A) \<noteq> {}"
-  let ?S = "fst`(nonzero_positions(Rep_matrix A))" 
+  let ?S = "fst`(nonzero_positions(Rep_matrix A))"
   from a have b: "?S \<noteq> {}" by (simp)
   have c: "finite (?S)" by (simp add: finite_nonzero_positions)
   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[OF c b]) 
+  have "m \<notin> ?S"
+    proof -
+      have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add: Max[OF c b])
       moreover from d have "~(m <= 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)
 qed
-text {* \matrix cool *}
+
 constdefs
   transpose_infmatrix :: "'a infmatrix \<Rightarrow> 'a infmatrix"
   "transpose_infmatrix A j i == A i j"
@@ -64,40 +64,40 @@
   apply (rule ext)+
   by (simp add: transpose_infmatrix_def)
 
-lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)" 
+lemma transpose_infmatrix_closed[simp]: "Rep_matrix (Abs_matrix (transpose_infmatrix (Rep_matrix x))) = transpose_infmatrix (Rep_matrix x)"
 apply (rule Abs_matrix_inverse)
 apply (simp add: matrix_def nonzero_positions_def image_def)
 proof -
   let ?A = "{pos. Rep_matrix x (snd pos) (fst pos) \<noteq> 0}"
   let ?swap = "% pos. (snd pos, fst pos)"
   let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
-  have swap_image: "?swap`?A = ?B" 
+  have swap_image: "?swap`?A = ?B"
     apply (simp add: image_def)
     apply (rule set_ext)
     apply (simp)
     proof
       fix y
-      assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)" 
-      thus "Rep_matrix x (fst y) (snd y) \<noteq> 0" 
-	proof -
-	  from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
-	  then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
-	qed 
+      assume hyp: "\<exists>a b. Rep_matrix x b a \<noteq> 0 \<and> y = (b, a)"
+      thus "Rep_matrix x (fst y) (snd y) \<noteq> 0"
+        proof -
+          from hyp obtain a b where "(Rep_matrix x b a \<noteq> 0 & y = (b,a))" by blast
+          then show "Rep_matrix x (fst y) (snd y) \<noteq> 0" by (simp)
+        qed
     next
       fix y
       assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
-      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" by (rule exI[of _ "snd y"], rule exI[of _ "fst y"], simp) 
+      show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))" by (rule exI[of _ "snd y"], rule exI[of _ "fst y"], simp)
     qed
-  then have "finite (?swap`?A)" 
+  then have "finite (?swap`?A)"
     proof -
       have "finite (nonzero_positions (Rep_matrix x))" by (simp add: finite_nonzero_positions)
       then have "finite ?B" by (simp add: nonzero_positions_def)
       with swap_image show "finite (?swap`?A)" by (simp)
-    qed    
+    qed
   moreover
   have "inj_on ?swap ?A" by (simp add: inj_on_def)
-  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A]) 	
-qed 
+  ultimately show "finite ?A"by (rule finite_imageD[of ?swap ?A])
+qed
 
 lemma transpose_matrix[simp]: "Rep_matrix(transpose_matrix A) j i = Rep_matrix A i j"
 by (simp add: transpose_matrix_def)
@@ -105,16 +105,16 @@
 lemma transpose_transpose_id[simp]: "transpose_matrix (transpose_matrix A) = A"
 by (simp add: transpose_matrix_def)
 
-lemma nrows_transpose[simp]: "nrows (transpose_matrix A) = ncols A" 
+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)
 
-lemma ncols_transpose[simp]: "ncols (transpose_matrix A) = nrows A" 
+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)
 
-lemma ncols: "ncols A <= n \<Longrightarrow> Rep_matrix A m n = 0" 
+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 "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
@@ -126,13 +126,13 @@
   let ?P = "nonzero_positions (Rep_matrix A)"
   let ?p = "snd`?P"
   have a:"finite ?p" by (simp add: finite_nonzero_positions)
-  let ?m = "Max ?p"  
+  let ?m = "Max ?p"
   assume "~(Suc (?m) <= n)"
   then have b:"n <= ?m" by (simp)
   fix a b
   assume "(a,b) \<in> ?P"
   then have "?p \<noteq> {}" by (auto)
-  with a have "?m \<in>  ?p" by (simp)   
+  with a have "?m \<in>  ?p" by (simp)
   moreover have "!x. (x \<in> ?p \<longrightarrow> (? y. (Rep_matrix A y x) \<noteq> 0))" by (simp add: nonzero_positions_def image_def)
   ultimately have "? y. (Rep_matrix A y ?m) \<noteq> 0" by (simp)
   moreover assume ?st
@@ -194,9 +194,9 @@
     let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
     let ?sd = "{pos. fst pos = m & snd pos < n}"
     assume f0: "finite ?s0"
-    have f1: "finite ?sd" 
+    have f1: "finite ?sd"
     proof -
-      let ?f = "% x. (m, x)"	
+      let ?f = "% x. (m, x)"
       have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
       moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
       ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
@@ -205,18 +205,18 @@
     from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
     with su show "finite ?s1" by (simp)
 qed
-    
-lemma RepAbs_matrix: 
+
+lemma RepAbs_matrix:
   assumes aem: "? m. ! j i. m <= j \<longrightarrow> x j i = 0" (is ?em) and aen:"? n. ! j i. (n <= i \<longrightarrow> x j i = 0)" (is ?en)
-  shows "(Rep_matrix (Abs_matrix x)) = x"  
+  shows "(Rep_matrix (Abs_matrix x)) = x"
 apply (rule Abs_matrix_inverse)
 apply (simp add: matrix_def nonzero_positions_def)
-proof -  
+proof -
   from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
-  from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)    
+  from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
   let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
   let ?v = "{pos. fst pos < m & snd pos < n}"
-  have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)  
+  have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
   from a b have "(?u \<inter> (-?v)) = {}"
     apply (simp)
     apply (rule set_ext)
@@ -228,21 +228,21 @@
   ultimately show "finite ?u" by (rule finite_subset)
 qed
 
-constdefs 
+constdefs
   apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix"
   "apply_infmatrix f == % A. (% j i. f (A j i))"
   apply_matrix :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix"
-  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))" 
+  "apply_matrix f == % A. Abs_matrix (apply_infmatrix f (Rep_matrix A))"
   combine_infmatrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix \<Rightarrow> 'c infmatrix"
-  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"   
+  "combine_infmatrix f == % A B. (% j i. f (A j i) (B j i))"
   combine_matrix :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a::zero) matrix \<Rightarrow> ('b::zero) matrix \<Rightarrow> ('c::zero) matrix"
   "combine_matrix f == % 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)
 
-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)   
+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)
 
 constdefs
 commutative :: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> bool"
@@ -250,15 +250,15 @@
 associative :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
 "associative f == ! x y z. f (f x y) z = f x (f y z)"
 
-text{* 
+text{*
 To reason about associativity and commutativity of operations on matrices,
 let's take a step back and look at the general situtation: Assume that we have
 sets $A$ and $B$ with $B \subset A$ and an abstraction $u: A \rightarrow B$. This abstraction has to fulfill $u(b) = b$ for all $b \in B$, but is arbitrary otherwise.
 Each function $f: A \times A \rightarrow A$ now induces a function $f': B \times B \rightarrow B$ by $f' = u \circ f$.
-It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$     
+It is obvious that commutativity of $f$ implies commutativity of $f'$: $f' x y = u (f x y) = u (f y x) = f' y x.$
 *}
 
-lemma combine_infmatrix_commute: 
+lemma combine_infmatrix_commute:
   "commutative f \<Longrightarrow> commutative (combine_infmatrix f)"
 by (simp add: commutative_def combine_infmatrix_def)
 
@@ -267,7 +267,7 @@
 by (simp add: combine_matrix_def commutative_def combine_infmatrix_def)
 
 text{*
-On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$, 
+On the contrary, given an associative function $f$ we cannot expect $f'$ to be associative. A counterexample is given by $A=\ganz$, $B=\{-1, 0, 1\}$,
 as $f$ we take addition on $\ganz$, which is clearly associative. The abstraction is given by  $u(a) = 0$ for $a \notin B$. Then we have
 \[ f' (f' 1 1) -1 = u(f (u (f 1 1)) -1) = u(f (u 2) -1) = u (f 0 -1) = -1, \]
 but on the other hand we have
@@ -281,7 +281,7 @@
 lemma finite_nonzero_positions_Rep[simp]: "finite (nonzero_positions (Rep_matrix A))"
 by (insert Rep_matrix [of A], simp add: matrix_def)
 
-lemma combine_infmatrix_closed [simp]: 
+lemma combine_infmatrix_closed [simp]:
   "f 0 0 = 0 \<Longrightarrow> Rep_matrix (Abs_matrix (combine_infmatrix f (Rep_matrix A) (Rep_matrix B))) = combine_infmatrix f (Rep_matrix A) (Rep_matrix B)"
 apply (rule Abs_matrix_inverse)
 apply (simp add: matrix_def)
@@ -314,7 +314,7 @@
 by (simp add: apply_matrix_def)
 
 lemma Rep_combine_matrix[simp]: "f 0 0 = 0 \<Longrightarrow> Rep_matrix (combine_matrix f A B) j i = f (Rep_matrix A j i) (Rep_matrix B j i)"
-  by(simp add: combine_matrix_def) 
+  by(simp add: combine_matrix_def)
 
 lemma combine_nrows: "f 0 0 = 0  \<Longrightarrow> nrows (combine_matrix f A B) <= max (nrows A) (nrows B)"
 by (simp add: nrows_le)
@@ -337,7 +337,7 @@
   "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
 
 consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
-primrec 
+primrec
   "foldseq f s 0 = s 0"
   "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
 
@@ -349,11 +349,11 @@
 lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
 proof -
   assume a:"associative f"
-  then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" 
+  then have sublemma: "!! n. ! N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
   proof -
     fix n
-    show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N" 
-    proof (induct n) 
+    show "!N s. N <= n \<longrightarrow> foldseq f s N = foldseq_transposed f s N"
+    proof (induct n)
       show "!N s. N <= 0 \<longrightarrow> foldseq f s N = foldseq_transposed f s N" by simp
     next
       fix n
@@ -361,43 +361,43 @@
       have c:"!!N s. N <= n \<Longrightarrow> foldseq f s N = foldseq_transposed f s N" by (simp add: b)
       show "! N t. N <= Suc n \<longrightarrow> foldseq f t N = foldseq_transposed f t N"
       proof (auto)
-	fix N t
-	assume Nsuc: "N <= Suc n"
-	show "foldseq f t N = foldseq_transposed f t N" 
-	proof cases 
-	  assume "N <= n"
-	  then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
-	next
-	  assume "~(N <= n)"
-	  with Nsuc have Nsuceq: "N = Suc n" by simp
-	  have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
-	  have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
-	  show "foldseq f t N = foldseq_transposed f t N"
-	    apply (simp add: Nsuceq)
-	    apply (subst c)
-	    apply (simp)
-	    apply (case_tac "n = 0")
-	    apply (simp)
-	    apply (drule neqz)
-	    apply (erule exE)
-	    apply (simp)
-	    apply (subst assocf)
-	    proof -
-	      fix m
-	      assume "n = Suc m & Suc m <= 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")
-		apply (subst c)
-		by simp+
-	      have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
-	      have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
-		apply (subst c)
-		by (simp add: mless)+
-	      have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
-	      from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
-	    qed
-	  qed
-	qed
+        fix N t
+        assume Nsuc: "N <= Suc n"
+        show "foldseq f t N = foldseq_transposed f t N"
+        proof cases
+          assume "N <= n"
+          then show "foldseq f t N = foldseq_transposed f t N" by (simp add: b)
+        next
+          assume "~(N <= n)"
+          with Nsuc have Nsuceq: "N = Suc n" by simp
+          have neqz: "n \<noteq> 0 \<Longrightarrow> ? m. n = Suc m & Suc m <= n" by arith
+          have assocf: "!! x y z. f x (f y z) = f (f x y) z" by (insert a, simp add: associative_def)
+          show "foldseq f t N = foldseq_transposed f t N"
+            apply (simp add: Nsuceq)
+            apply (subst c)
+            apply (simp)
+            apply (case_tac "n = 0")
+            apply (simp)
+            apply (drule neqz)
+            apply (erule exE)
+            apply (simp)
+            apply (subst assocf)
+            proof -
+              fix m
+              assume "n = Suc m & Suc m <= 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")
+                apply (subst c)
+                by simp+
+              have step2: "f (t 0) ?T2 = foldseq f t (Suc m)" (is "_ = ?T3") by simp
+              have step3: "?T3 = foldseq_transposed f t (Suc m)" (is "_ = ?T4")
+                apply (subst c)
+                by (simp add: mless)+
+              have step4: "?T4 = f (foldseq_transposed f t m) (t (Suc m))" (is "_=?T5") by simp
+              from step1 step2 step3 step4 show sowhat: "f (f (t 0) ?T1) (t (Suc (Suc m))) = f ?T5 (t (Suc (Suc m)))" by simp
+            qed
+          qed
+        qed
       qed
     qed
     show "foldseq f = foldseq_transposed f" by ((rule ext)+, insert sublemma, auto)
@@ -419,7 +419,7 @@
 
 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); ? x y. (f x) \<noteq> (f y); ? x y. (g x) \<noteq> (g y); f x x = x; g x x = x\<rbrakk> \<Longrightarrow> f=g | (! y. f y x = y) | (! y. g y x = y)"
 oops
-(* Model found 
+(* Model found
 
 Trying to find a model that refutes: \<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;
@@ -435,7 +435,7 @@
 f: (a0\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0), a1\<mapsto>(a0\<mapsto>a1, a1\<mapsto>a1, a2\<mapsto>a1), a2\<mapsto>(a0\<mapsto>a0, a1\<mapsto>a0, a2\<mapsto>a0))
 *)
 
-lemma foldseq_zero: 
+lemma foldseq_zero:
 assumes fz: "f 0 0 = 0" and sz: "! i. i <= n \<longrightarrow> s i = 0"
 shows "foldseq f s n = 0"
 proof -
@@ -446,7 +446,7 @@
   then show "foldseq f s n = 0" by (simp add: sz)
 qed
 
-lemma foldseq_significant_positions: 
+lemma foldseq_significant_positions:
   assumes p: "! i. i <= N \<longrightarrow> S i = T i"
   shows "foldseq f S N = foldseq f T N" (is ?concl)
 proof -
@@ -456,8 +456,8 @@
     apply (simp)
     apply (auto)
     proof -
-      fix n 
-      fix s::"nat\<Rightarrow>'a" 
+      fix n
+      fix s::"nat\<Rightarrow>'a"
       fix t::"nat\<Rightarrow>'a"
       assume a: "\<forall>s t. (\<forall>i\<le>n. s i = t i) \<longrightarrow> foldseq f s n = foldseq f t n"
       assume b: "\<forall>i\<le>Suc n. s i = t i"
@@ -467,20 +467,20 @@
     qed
   with p show ?concl by simp
 qed
-  
+
 lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")
 proof -
   have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
   have suc2: "!! a b. \<lbrakk>a <= Suc b; ~ (a <= b)\<rbrakk> \<Longrightarrow> a = (Suc b)" by arith
   have eq: "!! (a::nat) b. \<lbrakk>~(a < b); a <= b\<rbrakk> \<Longrightarrow> a = b" by arith
   have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
-  have "!! n. ! 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 "!! n. ! 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"
     apply (induct_tac n)
     apply (simp)
     apply (simp)
     apply (auto)
     apply (case_tac "m = Suc na")
-    apply (simp) 
+    apply (simp)
     apply (rule a)
     apply (rule foldseq_significant_positions)
     apply (simp, auto)
@@ -490,31 +490,31 @@
       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  
-      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 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
+      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> ? mm. m = Suc mm & mm <= na" by arith
       show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
         foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
-	apply (simp add: subd)
-	apply (case_tac "m=0")
-	apply (simp)
-	apply (drule sube)
-	apply (auto)
-	apply (rule a)
-	by (simp add: subc if_def)
+        apply (simp add: subd)
+        apply (case_tac "m=0")
+        apply (simp)
+        apply (drule sube)
+        apply (auto)
+        apply (rule a)
+        by (simp add: subc if_def)
     qed
-  then show "?p \<Longrightarrow> ?concl" by simp  
+  then show "?p \<Longrightarrow> ?concl" by simp
 qed
-	
+
 lemma foldseq_zerotail:
   assumes
-  fz: "f 0 0 = 0" 
-  and sz: "! i.  n <= i \<longrightarrow> s i = 0" 
-  and nm: "n <= m" 
+  fz: "f 0 0 = 0"
+  and sz: "! i.  n <= i \<longrightarrow> s i = 0"
+  and nm: "n <= m"
   shows
-  "foldseq f s n = foldseq f s m" 
+  "foldseq f s n = foldseq f s m"
 proof -
   have a: "!! a b. ~(a < b) \<Longrightarrow> a <= b \<Longrightarrow> (a::nat) = b" by simp
   show "foldseq f s n = foldseq f s m"
@@ -539,7 +539,7 @@
   have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
   have c: "0 <= m" by simp
   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
-  show ?concl 
+  show ?concl
     apply (subst foldseq_tail[OF nm])
     apply (rule foldseq_significant_positions)
     apply (auto)
@@ -555,9 +555,9 @@
     apply (auto)
     by (simp add: prems foldseq_zero)
 qed
-    
+
 lemma foldseq_zerostart:
-  "! x. f 0 (f 0 x) = f 0 x \<Longrightarrow>  ! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" 
+  "! x. f 0 (f 0 x) = f 0 x \<Longrightarrow>  ! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
 proof -
   assume f00x: "! x. f 0 (f 0 x) = f 0 x"
   have "! s. (! i. i<=n \<longrightarrow> s i = 0) \<longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))"
@@ -572,22 +572,22 @@
       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: "! i. i <= 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)+
+        apply (subst a)
+        apply (subst c)
+        by (simp add: d f00x)+
     qed
   then show "! i. i <= n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s (Suc n) = f 0 (s (Suc n))" by simp
 qed
 
 lemma foldseq_zerostart2:
-  "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n" 
+  "! x. f 0 x = x \<Longrightarrow>  ! i. i < n \<longrightarrow> s i = 0 \<Longrightarrow> foldseq f s n = s n"
 proof -
   assume a:"! i. i<n \<longrightarrow> s i = 0"
   assume x:"! x. f 0 x = x"
-  from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast  
+  from x have f00x: "! x. f 0 (f 0 x) = f 0 x" by blast
   have b: "!! i l. i < Suc l = (i <= l)" by arith
   have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
-  show "foldseq f s n = s n" 
+  show "foldseq f s n = s n"
   apply (case_tac "n=0")
   apply (simp)
   apply (insert a)
@@ -598,13 +598,13 @@
   apply (drule foldseq_zerostart)
   by (simp add: x)+
 qed
-   
-lemma foldseq_almostzero: 
+
+lemma foldseq_almostzero:
   assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
   shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
 proof -
   from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
-  from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp 
+  from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
   show ?concl
     apply auto
     apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
@@ -629,20 +629,20 @@
   then show ?concl by simp
 qed
 
-constdefs 
+constdefs
   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"
-  "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(% j i. foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) n)"
   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"
   "mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
 
-lemma mult_matrix_n: 
+lemma mult_matrix_n:
   assumes prems: "ncols A \<le>  n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
   shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
 proof -
   show ?concl using prems
     apply (simp add: mult_matrix_def mult_matrix_n_def)
     apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
-    by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems) 
+    by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
 qed
 
 lemma mult_matrix_nm:
@@ -653,29 +653,29 @@
   also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
   finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
 qed
-   
-constdefs 
+
+constdefs
   r_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
   "r_distributive fmul fadd == ! a u v. fmul a (fadd u v) = fadd (fmul a u) (fmul a v)"
   l_distributive :: "('a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
   "l_distributive fmul fadd == ! a u v. fmul (fadd u v) a = fadd (fmul u a) (fmul v a)"
   distributive :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> bool"
-  "distributive fmul fadd == l_distributive fmul fadd & r_distributive fmul fadd" 
+  "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 r_distributive_matrix:
- assumes prems: 
-  "r_distributive fmul fadd" 
-  "associative fadd" 
-  "commutative fadd" 
-  "fadd 0 0 = 0" 
-  "! a. fmul a 0 = 0" 
+ assumes prems:
+  "r_distributive fmul fadd"
+  "associative fadd"
+  "commutative fadd"
+  "fadd 0 0 = 0"
+  "! a. fmul a 0 = 0"
   "! a. fmul 0 a = 0"
  shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
 proof -
-  from prems show ?concl 
+  from prems show ?concl
     apply (simp add: r_distributive_def mult_matrix_def, auto)
     proof -
       fix a::"'a matrix"
@@ -684,38 +684,38 @@
       let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
       from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
         combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
-	apply (simp add: combine_matrix_def combine_infmatrix_def)
-	apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
-	apply (subst RepAbs_matrix)
-	apply (simp, auto)
-	apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
-	apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
-	apply (subst RepAbs_matrix)
-	apply (simp, auto)
-	apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
-	apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
-	done
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
+        apply (simp add: combine_matrix_def combine_infmatrix_def)
+        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
+        apply (subst RepAbs_matrix)
+        apply (simp, auto)
+        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
+        apply (rule exI[of _ "ncols v"], simp add: ncols_le foldseq_zero)
+        apply (subst RepAbs_matrix)
+        apply (simp, auto)
+        apply (rule exI[of _ "nrows a"], simp add: nrows_le foldseq_zero)
+        apply (rule exI[of _ "ncols u"], simp add: ncols_le foldseq_zero)
+        done
     qed
 qed
 
 lemma l_distributive_matrix:
- assumes prems: 
-  "l_distributive fmul fadd" 
-  "associative fadd" 
-  "commutative fadd" 
-  "fadd 0 0 = 0" 
-  "! a. fmul a 0 = 0" 
+ assumes prems:
+  "l_distributive fmul fadd"
+  "associative fadd"
+  "commutative fadd"
+  "fadd 0 0 = 0"
+  "! a. fmul a 0 = 0"
   "! a. fmul 0 a = 0"
  shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
 proof -
-  from prems show ?concl 
+  from prems show ?concl
     apply (simp add: l_distributive_def mult_matrix_def, auto)
     proof -
       fix a::"'b matrix"
@@ -724,32 +724,32 @@
       let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
       from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
                combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
-	apply (simp add: max1 max2 combine_nrows combine_ncols)+
-	apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
-	apply (simp add: combine_matrix_def combine_infmatrix_def)
-	apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
-	apply (subst RepAbs_matrix)
-	apply (simp, auto)
-	apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
-	apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
-	apply (subst RepAbs_matrix)
-	apply (simp, auto)
-	apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
-	apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
-	done
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+        apply (simp add: max1 max2 combine_nrows combine_ncols)+
+        apply (simp add: mult_matrix_n_def l_distributive_def foldseq_distr[of fadd])
+        apply (simp add: combine_matrix_def combine_infmatrix_def)
+        apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
+        apply (subst RepAbs_matrix)
+        apply (simp, auto)
+        apply (rule exI[of _ "nrows v"], simp add: nrows_le foldseq_zero)
+        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
+        apply (subst RepAbs_matrix)
+        apply (simp, auto)
+        apply (rule exI[of _ "nrows u"], simp add: nrows_le foldseq_zero)
+        apply (rule exI[of _ "ncols a"], simp add: ncols_le foldseq_zero)
+        done
     qed
 qed
 
-    
+
 instance matrix :: (zero)zero by intro_classes
 
 defs(overloaded)
-  zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)" 
+  zero_matrix_def: "(0::('a::zero) matrix) == Abs_matrix(% j i. 0)"
 
 lemma Rep_zero_matrix_def[simp]: "Rep_matrix 0 j i = 0"
   apply (simp add: zero_matrix_def)
@@ -767,7 +767,7 @@
   have a:"!! (x::nat). x <= 0 \<Longrightarrow> x = 0" by (arith)
   show "ncols 0 = 0" by (rule a, subst ncols_le, simp)
 qed
-  
+
 lemma combine_matrix_zero_r_neutral: "zero_r_neutral f \<Longrightarrow> zero_r_neutral (combine_matrix f)"
   by (simp add: zero_r_neutral_def combine_matrix_def combine_infmatrix_def)
 
@@ -816,7 +816,7 @@
 
 constdefs
   column_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
-  "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"  
+  "column_of_matrix A n == take_columns (move_matrix A 0 (- int n)) 1"
   row_of_matrix :: "('a::zero) matrix \<Rightarrow> nat \<Rightarrow> 'a matrix"
   "row_of_matrix A m == take_rows (move_matrix A (- int m) 0) 1"
 
@@ -845,7 +845,7 @@
 apply (subst nrows_le)
 by simp
 
-lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)" 
+lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
 apply (auto)
 apply (rule le_anti_sym)
 apply (subst ncols_le)
@@ -858,7 +858,7 @@
 apply (rule not_leE)
 apply (subst ncols_le)
 by simp
- 
+
 lemma combine_singleton: "f 0 0 = 0 \<Longrightarrow> combine_matrix f (singleton_matrix j i a) (singleton_matrix j i b) = singleton_matrix j i (f a b)"
 apply (simp add: singleton_matrix_def combine_matrix_def combine_infmatrix_def)
 apply (subst RepAbs_matrix)
@@ -870,8 +870,8 @@
 apply (rule exI[of _ "Suc i"], simp)
 by simp
 
-lemma Rep_move_matrix[simp]: 
-  "Rep_matrix (move_matrix A y x) j i = 
+lemma Rep_move_matrix[simp]:
+  "Rep_matrix (move_matrix A y x) j i =
   (if (neg ((int j)-y)) | (neg ((int i)-x)) then 0 else Rep_matrix A (nat((int j)-y)) (nat((int i)-x)))"
 apply (simp add: move_matrix_def)
 apply (auto)
@@ -881,7 +881,7 @@
 
 lemma Rep_take_columns[simp]:
   "Rep_matrix (take_columns A c) j i =
-  (if i < c then (Rep_matrix A j i) else 0)" 
+  (if i < c then (Rep_matrix A j i) else 0)"
 apply (simp add: take_columns_def)
 apply (subst RepAbs_matrix)
 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
@@ -890,7 +890,7 @@
 
 lemma Rep_take_rows[simp]:
   "Rep_matrix (take_rows A r) j i =
-  (if j < r then (Rep_matrix A j i) else 0)" 
+  (if j < r then (Rep_matrix A j i) else 0)"
 apply (simp add: take_rows_def)
 apply (subst RepAbs_matrix)
 apply (rule exI[of _ "nrows A"], auto, simp add: nrows_le)
@@ -941,7 +941,7 @@
   and fprems:
   "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
-  "! a. fadd a 0 = a" 
+  "! a. fadd a 0 = a"
   "! a. fadd 0 a = a"
   and contraprems:
   "mult_matrix fmul fadd A = mult_matrix fmul fadd B"
@@ -951,7 +951,7 @@
   assume a: "A \<noteq> B"
   have b: "!! f g. (! x y. f x y = g x y) \<Longrightarrow> f = g" by ((rule ext)+, auto)
   have "? j i. (Rep_matrix A j i) \<noteq> (Rep_matrix B j i)"
-    apply (rule contrapos_np[of "False"], simp+)    
+    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)
   then obtain J I where c:"(Rep_matrix A J I) \<noteq> (Rep_matrix B J I)" by blast
@@ -973,7 +973,7 @@
   foldmatrix :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
   "foldmatrix f g A m n == foldseq_transposed g (% j. foldseq f (A j) n) m"
   foldmatrix_transposed :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a infmatrix) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a"
-  "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 (% j. foldseq_transposed f (A j) n) m"
 
 lemma foldmatrix_transpose:
   assumes
@@ -983,31 +983,31 @@
 proof -
   have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
   have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
-    apply (induct n) 
+    apply (induct n)
     apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
     apply (auto)
     by (drule_tac x1="(% 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 (simp)
     apply (insert tworows)
     apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) na) else (A (Suc na) i))" in spec)
     by (simp add: foldmatrix_def foldmatrix_transposed_def)
 qed
 
 lemma foldseq_foldseq:
-assumes 
+assumes
   "associative f"
   "associative g"
-  "! a b c d. g(f a b) (f c d) = f (g a c) (g b d)" 
-shows 
+  "! 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"
   apply (insert foldmatrix_transpose[of g f A m n])
   by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
-  
-lemma mult_n_nrows: 
-assumes 
+
+lemma mult_n_nrows:
+assumes
 "! a. fmul 0 a = 0"
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
@@ -1021,8 +1021,8 @@
 apply (simp add: ncols prems foldseq_zero)
 by (simp add: nrows prems foldseq_zero)
 
-lemma mult_n_ncols: 
-assumes 
+lemma mult_n_ncols:
+assumes
 "! a. fmul 0 a = 0"
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
@@ -1036,8 +1036,8 @@
 apply (simp add: ncols prems foldseq_zero)
 by (simp add: ncols prems foldseq_zero)
 
-lemma mult_nrows: 
-assumes 
+lemma mult_nrows:
+assumes
 "! a. fmul 0 a = 0"
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
@@ -1045,7 +1045,7 @@
 by (simp add: mult_matrix_def mult_n_nrows prems)
 
 lemma mult_ncols:
-assumes 
+assumes
 "! a. fmul 0 a = 0"
 "! a. fmul a 0 = 0"
 "fadd 0 0 = 0"
@@ -1079,7 +1079,7 @@
     apply (rule ext)+
     apply (simp add: mult_matrix_def)
     apply (subst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"])
-    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+    
+    apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
     apply (subst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
     apply (subst mult_matrix_nm[of _ _ _ "?N"])
     apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
@@ -1107,8 +1107,8 @@
     apply (simp add: prems)+
     by (simp add: transpose_infmatrix)
 qed
- 
-lemma 
+
+lemma
   assumes prems:
   "! a. fmul1 0 a = 0"
   "! a. fmul1 a 0 = 0"
@@ -1123,7 +1123,7 @@
   "! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
   "! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
   shows
-  "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)" 
+  "(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
 apply (rule ext)+
 apply (simp add: comp_def )
 by (simp add: mult_matrix_assoc prems)
@@ -1141,7 +1141,7 @@
 proof -
   have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
     by (simp! add: associative_def commutative_def)
-  then show ?concl 
+  then show ?concl
     apply (subst mult_matrix_assoc)
     apply (simp_all!)
     by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
@@ -1157,26 +1157,26 @@
 apply (rule ext)+
 by simp
 
-lemma Rep_mult_matrix: 
-  assumes 
-  "! a. fmul 0 a = 0"  
+lemma Rep_mult_matrix:
+  assumes
+  "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
   "fadd 0 0 = 0"
   shows
-  "Rep_matrix(mult_matrix fmul fadd A B) j i = 
+  "Rep_matrix(mult_matrix fmul fadd A B) j i =
   foldseq fadd (% 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 (simp add: mult_matrix_def mult_matrix_n_def)
 apply (subst RepAbs_matrix)
 apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
 apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
 by simp
 
 lemma transpose_mult_matrix:
-  assumes 
-  "! a. fmul 0 a = 0"  
+  assumes
+  "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
   "fadd 0 0 = 0"
-  "! x y. fmul y x = fmul x y" 
+  "! 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])
@@ -1189,7 +1189,7 @@
   le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
   less_def: "(A::('a::{ord,zero}) matrix) < B == (A <= B) & (A \<noteq> B)"
 
-instance matrix :: ("{order, zero}") order  
+instance matrix :: ("{order, zero}") order
 apply intro_classes
 apply (simp_all add: le_matrix_def less_def)
 apply (auto)
@@ -1202,7 +1202,7 @@
 apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
 by simp
 
-lemma le_apply_matrix: 
+lemma le_apply_matrix:
   assumes
   "f 0 = 0"
   "! x y. x <= y \<longrightarrow> f x <= f y"
@@ -1224,20 +1224,20 @@
 lemma le_left_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b" 
+  "! a b c. 0 <= c & a <= b \<longrightarrow> f c a <= f c b"
   "0 <= C"
   "A <= B"
-  shows 
+  shows
   "combine_matrix f C A <= combine_matrix f C B"
   by (simp! add: le_matrix_def)
 
 lemma le_right_combine_matrix:
   assumes
   "f 0 0 = 0"
-  "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c" 
+  "! a b c. 0 <= c & a <= b \<longrightarrow> f a c <= f b c"
   "0 <= C"
   "A <= B"
-  shows 
+  shows
   "combine_matrix f A C <= combine_matrix f B C"
   by (simp! add: le_matrix_def)
 
@@ -1246,22 +1246,22 @@
 
 lemma le_foldseq:
   assumes
-  "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d" 
+  "! a b c d . a <= b & c <= d \<longrightarrow> f a c <= f b d"
   "! i. i <= n \<longrightarrow> s i <= t i"
   shows
   "foldseq f s n <= foldseq f t n"
 proof -
   have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!)
   then show "foldseq f s n <= foldseq f t n" by (simp!)
-qed  
+qed
 
 lemma le_left_mult:
   assumes
   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
   "! c a b. 0 <= c & a <= b \<longrightarrow> fmul c a <= fmul c b"
-  "! a. fmul 0 a = 0"  
+  "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
-  "fadd 0 0 = 0" 
+  "fadd 0 0 = 0"
   "0 <= C"
   "A <= B"
   shows
@@ -1276,9 +1276,9 @@
   assumes
   "! a b c d. a <= b & c <= d \<longrightarrow> fadd a c <= fadd b d"
   "! c a b. 0 <= c & a <= b \<longrightarrow> fmul a c <= fmul b c"
-  "! a. fmul 0 a = 0"  
+  "! a. fmul 0 a = 0"
   "! a. fmul a 0 = 0"
-  "fadd 0 0 = 0" 
+  "fadd 0 0 = 0"
   "0 <= C"
   "A <= B"
   shows
diff -r 9ead82084de8 -r d2c6a0f030ab src/HOL/Matrix/ROOT.ML
--- a/src/HOL/Matrix/ROOT.ML	Fri Apr 23 20:48:28 2004 +0200
+++ b/src/HOL/Matrix/ROOT.ML	Fri Apr 23 20:49:26 2004 +0200
@@ -1,1 +1,10 @@
+(*  Title:      HOL/Matrix/ROOT.ML
+    ID:         $Id$
+    Author:     Steven Obua
+    License:    2004 Technische Universität München
+
+Theory of matrices with an application of matrix theory to linear
+programming.
+*)
+
 use_thy "LinProg";
diff -r 9ead82084de8 -r d2c6a0f030ab src/HOL/Matrix/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/document/root.tex	Fri Apr 23 20:49:26 2004 +0200
@@ -0,0 +1,28 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}
+
+\begin{document}
+
+\title{Matrix}
+\author{Steven Obua}
+\maketitle
+
+%\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}