more bonus corr draft
authorlammich <lammich@in.tum.de>
Wed, 02 Aug 2017 17:11:04 +0200
changeset 69886 4abb5f2c0363
parent 69883 01e3de0b7352
child 69887 3880061ed9fb
more bonus corr
Exercises/exam/Q_Induction.thy
Exercises/hwsubm/OR/Biendarra_Julian_julian.biendarra@tum.de_632/matroids.thy
Exercises/hwsubm/OR/Haslbeck_Maximilian_max.haslbeck@mytum.de_640/Pell.thy
Exercises/hwsubm/OR/Kurz_Friedrich_friedrich.kurz@tum.de_646/be_original.thy
Exercises/hwsubm/OR/Madge_Pimentel_Fabio_fabio.madge@tum.de_659/SparseMatrix.thy
Exercises/hwsubm/OR/Rdle_Karl_Jonas_jonas.raedle@tum.de_652/Zipper.thy
Exercises/hwsubm/OR/Saporta_Antoine_Jacques_antoine.saporta@tum.de_631/Sparse_Matrix.thy
Exercises/hwsubm/OR/Stwe_Daniel_daniel.stuewe@tum.de_660/SkewBinHeap.thy
--- a/Exercises/exam/Q_Induction.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/exam/Q_Induction.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -55,6 +55,9 @@
 what are the three properties (goals) you have to prove?\<close>
 
 (*<*)  
+  
+thm g.induct  
+  
 end
 (*>*)  
 text_raw \<open>\blankpage\<close>
--- a/Exercises/hwsubm/OR/Biendarra_Julian_julian.biendarra@tum.de_632/matroids.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Biendarra_Julian_julian.biendarra@tum.de_632/matroids.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,4 +1,11 @@
+(** Score: 17/15
 
+  A formalisation of Matroids. Sensible definitions; a few basic properties were proven.
+  Some definitions are probably not ideal. The formalisation of the Greedy algorithm is
+  a nice result, but one would need a way to address nondeterminism to do it properly.
+  Several proofs are not trivial.
+
+*)
 (*\<Rightarrow>Manuel*)
 theory matroids
   imports Main
--- a/Exercises/hwsubm/OR/Haslbeck_Maximilian_max.haslbeck@mytum.de_640/Pell.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Haslbeck_Maximilian_max.haslbeck@mytum.de_640/Pell.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,21 +1,15 @@
-(*\<Rightarrow>Manuel*)
 (** Score: 20/15
+
+  Highly non-trivial mathematical proof. Some proofs more complicated than necessary.
+  Many steps are very ugly. Will make an excellent AFP entry after /major/ cleanup and
+  proofs of some more properties. Full disclosure: I suggested the topic and contributed
+  the indicated lemmas below.
+
 *)
 theory Pell
   imports Analysis
 begin
-
-(*
-The equation
-x^2 + n * y^2 = 1
-has integer solutions in x and y for every non-square n.
-*)
-
-(*
-- Only works with isabelle-dev
-- should also work with Complex Main, but first needs some minor refinements
-*)
-
+  
 (* Lemma by Manuel Eberl *)
 lemma nonneg_root_nat_or_irrat:
   assumes "x ^ 2 = real a" and "x \<ge> 0"
@@ -931,5 +925,4 @@
 qed
 
   end
-end
-
+end
\ No newline at end of file
--- a/Exercises/hwsubm/OR/Kurz_Friedrich_friedrich.kurz@tum.de_646/be_original.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Kurz_Friedrich_friedrich.kurz@tum.de_646/be_original.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,10 +1,17 @@
-(*\<Rightarrow> Simon*)
+(** Score: 11/15
+
+- Sparse matrices as lists of sparse vectors \<rightarrow> Makes it a bit easier than 'fully' sparse matrices
+- Initial definitions seem to be apt but sometimes a bit clumsy
+- It is shown that the function mapping matrices to their sparse versions is correct
+- Incomplete proof attempt to show equivalence of the two versions of matrix addition
+
+*)
 theory be_original
-  imports 
+  imports
     Main
     "~~/src/HOL/Matrix_LP/Matrix"
     "~~/src/HOL/Matrix_LP/SparseMatrix"
-    "../../../Public/Thys/Heap_Prelim"
+    "Heap_Prelim"
 begin
 
 text {* \ExerciseSheet{11}{7.~7.~2017} *}
@@ -15,17 +22,17 @@
 
   \<^item> This homework is for 3 weeks, and will yield 15 points + 15 bonus points.
   \<^item> You may develop a formalization from all areas, not only functional data structures.
-  \<^item> Set yourself a time frame and some intermediate/minimal goals. 
+  \<^item> Set yourself a time frame and some intermediate/minimal goals.
     Your formalization needs not be universal and complete after 3 weeks.
   \<^item> You are welcome to discuss the realizability of your project with the tutor!
-  \<^item> In case you should need inspiration to find a project: Sparse matrices, skew binary numbers, 
-    arbitrary precision arithmetic (on lists of bits), interval data structures (e.g. interval lists), 
+  \<^item> In case you should need inspiration to find a project: Sparse matrices, skew binary numbers,
+    arbitrary precision arithmetic (on lists of bits), interval data structures (e.g. interval lists),
     spatial data structures (quad-trees, oct-trees), Fibonacci heaps, etc.
 
 \<close>
 
 text \<open>
-In this theory simple dense and sparse matrix implementations using lists are being compared. 
+In this theory simple dense and sparse matrix implementations using lists are being compared.
 
   \<^item> dense matrix: implemented as a pair containing the dimensions and a list of dense vectors
   \<^item> dense vector: implemented as a pair containing the vector size and a list of real values
@@ -33,19 +40,19 @@
   \<^item> sparse vector: implemented as a pair containing the vector size and a list pairs of index and a real value (which is never zero)
 
 As the central result it is shown that dense and sparse matrix addition are interchangeable (lemma "condense_preserves_matrix_addition"): i.e.
-  
+
   condenseM (addM_LIL M N) = addM_SP (condenseM M) (condenseM N)
 
-The proof recurs on the interchangeability of dense and sparse vector addition which could however not be shown completely. 
+The proof recurs on the interchangeability of dense and sparse vector addition which could however not be shown completely.
 
-Additional operations (vector scalar multiplication, vector scalar product, vector multiplication for matrices and matrix multiplication) have been defined but could not be proven within the given time frame.  
+Additional operations (vector scalar multiplication, vector scalar product, vector multiplication for matrices and matrix multiplication) have been defined but could not be proven within the given time frame.
 \<close>
 
 
 
 (*
  * I. List of List Matrices (LIL Matrices).
- *)  
+ *)
 section "List of List Matrices (LIL Matrices)"
 subsection "Definitions"
 subsubsection "Ancillary definitions"
@@ -53,10 +60,10 @@
 fun repeat :: "'a \<Rightarrow> nat \<Rightarrow> 'a list" where
   "repeat a 0 = []"
 | "repeat a (Suc m) = (a # repeat a m)"
-    
+
 value "take 0 (repeat 1 10)"
 
-definition list_scalarProd :: "real list \<Rightarrow> real list \<Rightarrow> real" where 
+definition list_scalarProd :: "real list \<Rightarrow> real list \<Rightarrow> real" where
   "list_scalarProd l1 l2 \<equiv> sum_list (map (\<lambda> (a, a'). a * a') (zip l1 l2))"
 
 value "list_scalarProd [1..10] [1..5]"
@@ -65,7 +72,7 @@
 
 subsubsection "LIL Matrix and List Vector."
 paragraph "Basic definitions of LIL Matrix and List Vector."
-  
+
 text\<open>A simple list vector.\<close>
 type_synonym vector_LIL = "(nat * real list)"
 
@@ -73,28 +80,28 @@
 type_synonym matrix_LIL = "((nat * nat) * vector_LIL list)"
 
 
-  
+
 paragraph "LIL Matrix and List Vector Helper Functions."
-  
+
 abbreviation to_list :: "vector_LIL \<Rightarrow> real list" where
   "to_list V \<equiv> snd V"
-  
+
 abbreviation size_of :: "vector_LIL \<Rightarrow> nat" where
   "size_of V \<equiv> fst V"
 
 definition column_size_of :: "matrix_LIL \<Rightarrow> nat" where
   "column_size_of M = (fst \<circ> fst) M"
-  
+
 abbreviation row_size_of :: "matrix_LIL \<Rightarrow> nat" where
   "row_size_of M \<equiv> (snd \<circ> fst) M"
-  
+
 abbreviation to_rows :: "matrix_LIL \<Rightarrow> vector_LIL list" where
   "to_rows M \<equiv> snd M"
-  
+
 definition to_columns :: "matrix_LIL \<Rightarrow> vector_LIL list" where
-"to_columns M = (let rows = to_rows M; n = row_size_of M in 
+"to_columns M = (let rows = to_rows M; n = row_size_of M in
   map (\<lambda> j. (n, map (\<lambda> i. (to_list (rows ! i)) ! j) [0..<n])) [0..<column_size_of M]
-)" 
+)"
 
 value "to_columns ((3, 3), [(3, [1, 0, 0]), (3, [1, 0, 0]), (3, [1, 0, 0])])"
 
@@ -102,21 +109,21 @@
   "zeroV_LIL m = (m, repeat 0 m)"
 
 value "zeroV_LIL 3"
-  
+
 definition unitV_LIL :: "nat \<Rightarrow> nat \<Rightarrow> vector_LIL" where
   "unitV_LIL m i \<equiv> (if i \<ge> m
     then undefined
     else (m, (repeat 0 m)[i := 1])
   )"
-  
+
 value "unitV_LIL 3 0"
 value "unitV_LIL 3 4"
-  
-definition zeroM_LIL :: "nat \<Rightarrow> nat \<Rightarrow> matrix_LIL" where 
+
+definition zeroM_LIL :: "nat \<Rightarrow> nat \<Rightarrow> matrix_LIL" where
   "zeroM_LIL m n = ((m, n), map (\<lambda> _. zeroV_LIL m) [1..n])"
 
 value "zeroM_LIL 3 3"
-  
+
 definition identityM_LIL :: "nat \<Rightarrow> matrix_LIL" where
   "identityM_LIL m = ((m, m), map (\<lambda> i. unitV_LIL m i) [0..<m])"
 
@@ -128,57 +135,57 @@
 
 text\<open>List vector invariant.\<close>
 definition invarV_LIL :: "vector_LIL \<Rightarrow> bool" where
-  "invarV_LIL V \<equiv> (length (to_list V) = size_of V)"  
-  
+  "invarV_LIL V \<equiv> (length (to_list V) = size_of V)"
+
 text "LIL matrix invariant: the stored and actual number of rows are equal and for all rows the stored and actual number of columns are equal."
-definition invarM_LIL :: "matrix_LIL \<Rightarrow> bool" where 
-  "invarM_LIL M \<equiv> (let m = column_size_of M; n = row_size_of M; rows = to_rows M in 
+definition invarM_LIL :: "matrix_LIL \<Rightarrow> bool" where
+  "invarM_LIL M \<equiv> (let m = column_size_of M; n = row_size_of M; rows = to_rows M in
     n = length rows & (\<forall>v\<in>set rows. m = size_of v & invarV_LIL v)
   )"
 
 
 
 paragraph "Operations on LIL vectors."
-  
-definition insertV_LIL :: "vector_LIL \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> vector_LIL" where  
+
+definition insertV_LIL :: "vector_LIL \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> vector_LIL" where
   "insertV_LIL v i x \<equiv> (let k = size_of v in
     (if i \<ge> k
       then undefined
       else (k, (to_list v)[i := x])
     )
   )"
-  
-definition retrieveV_LIL :: "vector_LIL \<Rightarrow> nat \<Rightarrow> real option" where  
+
+definition retrieveV_LIL :: "vector_LIL \<Rightarrow> nat \<Rightarrow> real option" where
   "retrieveV_LIL v i \<equiv> (let k = size_of v in
     (if i \<ge> k
       then None
       else Some ((to_list v) ! i)
     )
   )"
-  
+
 definition addV_LIL :: "vector_LIL \<Rightarrow> vector_LIL \<Rightarrow> vector_LIL" where
   "addV_LIL v w \<equiv> (let k1 = size_of v; k2 = size_of w in
-    (if k1 = k2 
+    (if k1 = k2
       then (k1, map (\<lambda> (a, b). a + b) (zip (to_list v) (to_list w)))
       else undefined
     )
   )"
-  
+
 value "addV_LIL (zeroV_LIL 3) (unitV_LIL 3 0)"
-value "addV_LIL (unitV_LIL 3 2) (addV_LIL (unitV_LIL 3 0) (unitV_LIL 3 1))" 
+value "addV_LIL (unitV_LIL 3 2) (addV_LIL (unitV_LIL 3 0) (unitV_LIL 3 1))"
 value "addV_LIL (zeroV_LIL 3) (unitV_LIL 4 0)"
 
 definition scalarMultV_LIL :: "vector_LIL \<Rightarrow> real \<Rightarrow> vector_LIL" where
   "scalarMultV_LIL v a \<equiv> (let k = size_of v in
     (k, map (op * a) (to_list v))
   )"
-  
+
 definition scalarProdV_LIL :: "vector_LIL \<Rightarrow> vector_LIL \<Rightarrow> real" where
   "scalarProdV_LIL v w \<equiv> (if size_of v = size_of w
     then list_scalarProd (to_list v) (to_list w)
     else undefined
   )"
-  
+
 value "scalarProdV_LIL (4, [1, 1, 1, 1]) (4, [1..4])"
 value "scalarProdV_LIL (5, [1..5]) (4, [1..4])"
 
@@ -186,59 +193,59 @@
 
 paragraph "Operations on LIL matrices."
 
-text \<open>Insert the given element at the given row and column indexes (in case they don't exceed the matrix' row and column sizes).\<close>  
+text \<open>Insert the given element at the given row and column indexes (in case they don't exceed the matrix' row and column sizes).\<close>
 fun insertM_LIL :: "matrix_LIL \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> matrix_LIL" where
-  "insertM_LIL M i j x = (let m = column_size_of M; n = row_size_of M; l = to_rows M in 
+  "insertM_LIL M i j x = (let m = column_size_of M; n = row_size_of M; l = to_rows M in
     if i \<ge> n | j \<ge> m
     then undefined
     else ((m, n), l[i := insertV_LIL (l ! i) j x])
   )"
 
-value "insertM_LIL (zeroM_LIL 3 3) 0 0 1"  
+value "insertM_LIL (zeroM_LIL 3 3) 0 0 1"
 value "insertM_LIL (zeroM_LIL 3 3) 1 2 1"
 value "insertM_LIL (zeroM_LIL 3 3) 2 0 1"
-  
+
 definition retrieveM_LIL :: "matrix_LIL \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real option" where
-  "retrieveM_LIL M i j \<equiv> (let m = column_size_of M; n = row_size_of M in 
+  "retrieveM_LIL M i j \<equiv> (let m = column_size_of M; n = row_size_of M in
     (if i \<ge> n | j \<ge> m
       then None
       else retrieveV_LIL (to_rows M ! i) j
     )
   )"
-  
+
 value "retrieveM_LIL (zeroM_LIL 3 3) 2 2"
-value "retrieveM_LIL (zeroM_LIL 100 200) 200 3"  
-  
-text \<open>LIL Matrix Addition.\<close> 
-definition addM_LIL :: "matrix_LIL \<Rightarrow> matrix_LIL \<Rightarrow> matrix_LIL" where 
+value "retrieveM_LIL (zeroM_LIL 100 200) 200 3"
+
+text \<open>LIL Matrix Addition.\<close>
+definition addM_LIL :: "matrix_LIL \<Rightarrow> matrix_LIL \<Rightarrow> matrix_LIL" where
   "addM_LIL M N \<equiv> (let m1 = column_size_of M; m2 = column_size_of N; n1 = row_size_of M; n2 = row_size_of N in
     (if m1 = m2 & n1 = n2
       then ((m1, n1), map (\<lambda> (v1, v2). addV_LIL v1 v2) (zip (to_rows M) (to_rows N)))
       else undefined
     )
   )"
-  
+
 value "addM_LIL (identityM_LIL 3) (zeroM_LIL 3 3)"
 value "addM_LIL (identityM_LIL 3) (identityM_LIL 3)"
 value "addM_LIL (identityM_LIL 3) (zeroM_LIL 4 4)"
 
-definition scalarMultM_LIL :: "matrix_LIL \<Rightarrow> real \<Rightarrow> matrix_LIL" where 
+definition scalarMultM_LIL :: "matrix_LIL \<Rightarrow> real \<Rightarrow> matrix_LIL" where
   "scalarMultM_LIL M a \<equiv> (let m = column_size_of M; n = row_size_of M in
     ((m, n), map (\<lambda> v. scalarMultV_LIL v a) (to_rows M))
   )"
-  
+
 value "scalarMultM_LIL (identityM_LIL 3) 2"
 value "scalarMultM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 2"
-  
+
 definition vectorMultM_LIL :: "matrix_LIL \<Rightarrow> vector_LIL \<Rightarrow> vector_LIL" where
-  "vectorMultM_LIL M v = (let m = column_size_of M; k = size_of v in 
+  "vectorMultM_LIL M v = (let m = column_size_of M; k = size_of v in
     (if m = k
       then (k, map (scalarProdV_LIL v) (to_rows M))
       else undefined
     )
   )"
 
-value "insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9" 
+value "insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9"
 value "vectorMultM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9) (3, [1, 1, 1])"
 
 definition matrixMultM_LIL :: "matrix_LIL \<Rightarrow> matrix_LIL \<Rightarrow> matrix_LIL" where
@@ -251,7 +258,7 @@
 
 value "matrixMultM_LIL (identityM_LIL 3) (zeroM_LIL 3 3)"
 value "matrixMultM_LIL (identityM_LIL 3) (identityM_LIL 3)"
-value "matrixMultM_LIL (identityM_LIL 3) ((1, 3), [(1, [1]), (1, [1]), (1, [1])])"  
+value "matrixMultM_LIL (identityM_LIL 3) ((1, 3), [(1, [1]), (1, [1]), (1, [1])])"
 value "(insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9)"
 value "matrixMultM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9)"
 value "matrixMultM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (insertM_LIL (zeroM_LIL 3 3) 0 0 1) 0 1 2) 0 2 3) 1 0 4) 1 1 5) 1 2 6) 2 0 7) 2 1 8) 2 2 9) (zeroM_LIL 3 3)"
@@ -261,52 +268,52 @@
 subsection \<open>Proofs\<close>
 subsubsection \<open>Proofs w.r.t. LIL matrix implementation\<close>
 paragraph \<open>Some ancillary proofs concerning the properties of the helper functions.\<close>
-  
-lemma[simp]: "\<lbrakk>M = ((m, n), l)\<rbrakk> \<Longrightarrow> column_size_of M = m" 
-  unfolding column_size_of_def 
+
+lemma[simp]: "\<lbrakk>M = ((m, n), l)\<rbrakk> \<Longrightarrow> column_size_of M = m"
+  unfolding column_size_of_def
   by simp
-lemma[simp]: "\<lbrakk>M = ((m, n), l)\<rbrakk> \<Longrightarrow> row_size_of M = n" 
+lemma[simp]: "\<lbrakk>M = ((m, n), l)\<rbrakk> \<Longrightarrow> row_size_of M = n"
   by simp
-lemma[simp]: "\<lbrakk>V = (m, l)\<rbrakk> \<Longrightarrow> size_of V = m" 
+lemma[simp]: "\<lbrakk>V = (m, l)\<rbrakk> \<Longrightarrow> size_of V = m"
   by simp
-  
+
 text \<open>Proofs concerning properties of `[1..j]` with respect to `length`.\<close>
-thm upto.simps 
+thm upto.simps
 lemma length_upto_nonneg: "\<lbrakk>m \<ge> 0\<rbrakk> \<Longrightarrow> length [1..1 + m] = 1 + length [1..m]"
   apply (induction m)
   apply (auto simp add: upto_rec2)
   done
-  
-lemma length_upto_to_card: "length [1..m] = card (set [1..m])"   
+
+lemma length_upto_to_card: "length [1..m] = card (set [1..m])"
 proof (induction m)
   case (nonneg n)
-  then show ?case 
+  then show ?case
     proof (induction n)
       case 0
         then show ?case proof -
-        have "length [1..0] = card (set [1..0])" 
+        have "length [1..0] = card (set [1..0])"
           by simp
-        then have "length [] = card (set [])" 
+        then have "length [] = card (set [])"
           by simp
         then have "0 = card {}"
           by simp
         then show ?case
           by simp
-        qed   
+        qed
       next case (Suc m)
         then show ?case proof -
           assume PREM: "length [1..m] = card (set [1..m])"
-          have "card (set [1..(Suc m)]) = (card (set [1..m] \<union> set [Suc m]))" 
+          have "card (set [1..(Suc m)]) = (card (set [1..m] \<union> set [Suc m]))"
             by simp
           also have "\<dots> = card (set [1..m]) + card {Suc m}" using Finite_Set.card_Un_disjoint
             by auto
-          also have "\<dots> = length [1..m] + 1" 
+          also have "\<dots> = length [1..m] + 1"
             using PREM
             by simp
-          also have "\<dots> = length [1..(Suc m)]" 
-            using length_upto_nonneg 
+          also have "\<dots> = length [1..(Suc m)]"
+            using length_upto_nonneg
             by simp
-          finally show ?case 
+          finally show ?case
             by simp
         qed
     qed
@@ -314,32 +321,32 @@
     then show ?case by simp
   qed
 
-corollary length_upto: "length [1..m] = m" 
+corollary length_upto: "length [1..m] = m"
   by (simp add: length_upto_to_card)
-   
+
 lemma length_upto_suc:
   assumes "length [1..m] = m"
   shows  "length [1..1 + m] = 1 + m"
 proof -
-  have "length [1..Suc m] = card (set [1..Suc m])" 
+  have "length [1..Suc m] = card (set [1..Suc m])"
     using length_upto_to_card
     by blast
-  also have "\<dots> = Suc m" 
+  also have "\<dots> = Suc m"
     by simp
-  finally show ?thesis 
+  finally show ?thesis
     by (simp add: length_upto_to_card)
 qed
-    
-  
+
+
 
 text \<open>Example proofs of the respective invariants for zero vector and zero matrix.\<close>
-    
-    
+
+
 paragraph "Proof of operation properties"
 
 (*
 text "Show that insertion preserves the LIL matrix invariant."
-lemma insertm_lil_invar: 
+lemma insertm_lil_invar:
   assumes INVAR: "invarM_LIL M"
   assumes "i < row_size_of M"
   assumes "j < column_size_of M"
@@ -350,7 +357,7 @@
   obtain l where "l = (to_rows (insertM_LIL M i j x))" by blast
   have "insertM_LIL ((m, n), l) i j x = ((m, n), l[i := (l ! i)[j := x]])"
     by (smt B \<open>m = column_size_of (insertM_LIL M i j x)\<close> \<open>n = row_size_of (insertM_LIL M i j x)\<close> column_size_of_def comp_def fst_conv insertM_LIL.simps not_less snd_conv)
-  then have "invarM_LIL (insertM_LIL ((m, n), l) i j x) = invarM_LIL ((m, n), l[i := (l ! i)[j := x]])" 
+  then have "invarM_LIL (insertM_LIL ((m, n), l) i j x) = invarM_LIL ((m, n), l[i := (l ! i)[j := x]])"
     by simp
   then show ?thesis
     by (smt assms column_size_of_def comp_apply in_set_conv_nth insertM_LIL.simps invarM_LIL_def length_list_update nth_list_update_eq nth_list_update_neq prod.sel(1) prod.sel(2))
@@ -358,30 +365,30 @@
 
 text \<open>Show that for a matrix conforming to the invariant and a pair of indexes within the matrix bounds the sequence of insertion and retrieval at the same indexes yields the inserted value (represented as \texttt{Some x}).\<close>
 lemma retrieve_after_insertm:
-  assumes "invarM_LIL M" 
+  assumes "invarM_LIL M"
   assumes "i < row_size_of M"
   assumes "j < column_size_of M"
   shows "(Some x) = retrieveM_LIL (insertM_LIL M i j x) i j"
 proof -
-  obtain l where "l = to_rows M" 
+  obtain l where "l = to_rows M"
     by blast
   obtain m n l' where "((m, n), l') = insertM_LIL M i j x" and "l' = l[i := (l ! i)[j := x]]"
     by (smt \<open>l = to_rows M\<close> assms(2) assms(3) insertM_LIL.simps not_less)
   have "retrieveM_LIL (insertM_LIL M i j x) i j = retrieveM_LIL ((m, n), l') i j"
     by (simp add: \<open>((m, n), l') = insertM_LIL M i j x\<close>)
-  hence "retrieveM_LIL (insertM_LIL M i j x) i j = Some ((l' ! i) ! j)" 
+  hence "retrieveM_LIL (insertM_LIL M i j x) i j = Some ((l' ! i) ! j)"
     by (smt \<open>((m, n), l') = insertM_LIL M i j x\<close> assms(2) assms(3) insertM_LIL.simps not_less prod.sel(2) retrieveM_LIL.simps)
   hence "retrieveM_LIL (insertM_LIL M i j x) i j = Some ((l[i := (l ! i)[j := x]]) ! i ! j)"
-    using \<open>l' = l[i := (l ! i)[j := x]]\<close> 
+    using \<open>l' = l[i := (l ! i)[j := x]]\<close>
     by blast
   hence "retrieveM_LIL (insertM_LIL M i j x) i j = Some x"
     using assms
     by (metis \<open>l = to_rows M\<close> invarM_LIL_def nth_list_update nth_mem)
-  thus ?thesis 
+  thus ?thesis
     by simp
 qed
 
-text "Proof the matrix size property of matrix multiplication."  
+text "Proof the matrix size property of matrix multiplication."
 lemma matrixmult_lil_size:
   assumes "invarM_LIL M"
   assumes "invarM_LIL N"
@@ -398,9 +405,9 @@
   assumes "column_size_of M = row_size_of N"
   shows "invarM_LIL (matrixMultM_LIL M N)"
 proof -
-  obtain MN where "MN = matrixMultM_LIL M N" 
+  obtain MN where "MN = matrixMultM_LIL M N"
     by simp
-  have A: "row_size_of MN = row_size_of M" 
+  have A: "row_size_of MN = row_size_of M"
     using matrixmult_lil_size assms `MN = matrixMultM_LIL M N`
     by simp
   have B: "column_size_of MN = column_size_of N"
@@ -422,7 +429,7 @@
 
 (*
  * II. Sparse Matrices.
- *)  
+ *)
 section "Sparse Matrices"
 subsection "Definitions"
 subsubsection "Sparse Matrix and Sparse Vector"
@@ -430,19 +437,19 @@
 type_synonym listVector_SP = "(nat * real) list"
 type_synonym vector_SP = "(nat * listVector_SP)"
 type_synonym matrix_SP = "((nat * nat) * vector_SP list)"
-  
+
 definition zeroM_SP :: "nat \<Rightarrow> nat \<Rightarrow> matrix_SP" where
   "zeroM_SP m n = ((m, n), repeat (m, []) n)"
-  
+
 definition zeroV_SP :: "nat \<Rightarrow> vector_SP" where
   "zeroV_SP m = (m, Nil)"
-  
+
 value "zeroV_SP 3"
-  
+
 definition identityM_SP :: "nat \<Rightarrow> matrix_SP" where
   "identityM_SP m = ((m, m), map (\<lambda> i. (m, [(i, 1)]))  [0..<m])"
-  
-value "identityM_SP 3" 
+
+value "identityM_SP 3"
 
 definition condenseV :: "vector_LIL \<Rightarrow> vector_SP" where
   "condenseV v \<equiv> (let k = size_of v; l = to_list v in
@@ -452,16 +459,16 @@
 value "condenseV (4, [0, 0, 1, 0])"
 value "map condenseV [(4, [1, 0, 0, 0]), (4, [0, 1, 0, 0]), (4, [0, 0, 1, 0]), (4, [0, 0, 0, 1])]"
 
-definition condenseM :: "matrix_LIL \<Rightarrow> matrix_SP" where  
+definition condenseM :: "matrix_LIL \<Rightarrow> matrix_SP" where
   "condenseM M \<equiv> (let m = column_size_of M; n = row_size_of M; rows = to_rows M in
     ((m, n), map condenseV rows)
   )"
-  
-  
-  
+
+
+
 subsubsection "Operations"
 paragraph "Operations on sparse vectors."
-  
+
 definition indexesLV_SP :: "listVector_SP \<Rightarrow> nat list" where
   "indexesLV_SP l = (map fst l)"
 
@@ -478,7 +485,7 @@
 fun insertV_SP' :: "listVector_SP \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> listVector_SP" where
   "insertV_SP' [] i x = [(i, x)]"
 | "insertV_SP' ((i', x') # rest) i x = (if i' = i
-    then (i, x) # rest 
+    then (i, x) # rest
     else (if i' > i
       then ((i, x) # (i', x') # rest)
       else (i', x') # (insertV_SP' rest i x)
@@ -488,20 +495,20 @@
   "insertV_SP v i x \<equiv> (let k = size_of_SP v in
     (if i \<ge> k then undefined else (k, insertV_SP' (to_list_SP v) i x))
   )"
-  
+
 value "insertV_SP (1, []) 3 1"
-value "insertV_SP (3, []) 2 1"  
-value "insertV_SP (3, [(0, 1), (2, 3)]) 1 2"  
-value "insertV_SP (3, [(0, 1), (1, 2)]) 2 3"  
-  
+value "insertV_SP (3, []) 2 1"
+value "insertV_SP (3, [(0, 1), (2, 3)]) 1 2"
+value "insertV_SP (3, [(0, 1), (1, 2)]) 2 3"
+
 definition retrieveV_SP :: "vector_SP \<Rightarrow> nat \<Rightarrow> (nat * real) option" where
   "retrieveV_SP v i \<equiv> (if i \<ge> (size_of_SP v)
     then undefined
     else find (\<lambda> (index, x). index = i) (to_list_SP v))"
-  
+
 value "retrieveV_SP (3, []) 1"
 value "retrieveV_SP (3, [(2, 1)]) 2"
-  
+
 text "Helper function for vector addition."
 fun addV_SP' :: "listVector_SP \<Rightarrow> listVector_SP \<Rightarrow> listVector_SP" where
   "addV_SP' [] [] = []"
@@ -521,18 +528,18 @@
     then (size_of_SP v, addV_SP' (to_list_SP v) (to_list_SP w))
     else undefined
   )"
-  
+
 value "addV_SP (zeroV_SP 3) (zeroV_SP 3)"
 value "addV_SP (4, [(0, 1), (2, 1)]) (4, [(1, 1), (3, 1)])"
 value "addV_SP (4, [(1, 1), (3, 1)]) (4, [(0, 1), (2, 1)])"
 value "addV_SP (4, [(0, 1), (1, 1), (2, 1), (3, 1)]) (4, [(0, 1), (1, 1), (2, 1), (3, 1)])"
-  
+
 definition scalarMultV_SP :: "vector_SP \<Rightarrow> real \<Rightarrow> vector_SP" where
   "scalarMultV_SP v a \<equiv> (size_of_SP v, map (\<lambda> (i, x). (i, x * a)) (to_list_SP v))"
 
 value "scalarMultV_SP (zeroV_SP 3) 100"
-value "scalarMultV_SP (3, [(0, 1), (1, 1), (2,1)]) 2"  
-  
+value "scalarMultV_SP (3, [(0, 1), (1, 1), (2,1)]) 2"
+
 text \<open>
   Helper function for sparse vector product.
   The product is only calculated when indices match. Otherwise the entry for the smaller index is dropped because due to ordering there cannot be a matching index in the second list vector as the entry for the lowest index is already higher.
@@ -551,12 +558,12 @@
     then sum_list (scalarProdV_SP' (to_list_SP v) (to_list_SP w))
     else undefined
   )"
-  
+
 value "scalarProdV_SP (4, [(0,1), (2, 1)]) (4, [(1,1), (3,1)])"
 value "scalarProdV_SP (4, [(0,1), (1, 2), (2, 3), (3, 4)]) (4, [(0, 1), (1,1), (2, 1), (3,1)])"
 
 
-  
+
 paragraph "Operations on sparse matrices."
 
 definition column_size_of_SP :: "matrix_SP \<Rightarrow> nat" where
@@ -569,36 +576,36 @@
   "to_rows_SP M \<equiv> snd M"
   thm is_none_simps
 
-text \<open>Insert the given element at the given row and column indexes (in case they don't exceed the matrix' row and column sizes).\<close>  
+text \<open>Insert the given element at the given row and column indexes (in case they don't exceed the matrix' row and column sizes).\<close>
 definition insertM_SP :: "matrix_SP \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real \<Rightarrow> matrix_SP" where
   "insertM_SP M i j x \<equiv> (let m = column_size_of_SP M; n = row_size_of_SP M in
-    (if i < m & j < n 
+    (if i < m & j < n
       then (let rows = to_rows_SP M; row' = (insertV_SP (rows ! i) j x) in
         ((m, n), rows[i:=row'])
       )
       else undefined
     ))"
-  
+
 value "insertM_SP (zeroM_SP 3 3) 0 0 1"
 value "(insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 0 1) 1 0 1) 2 0 1)"
-  
+
 definition retrieveM_SP :: "matrix_SP \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> real option" where
   "retrieveM_SP M i j \<equiv> (case find ((op = j) \<circ> fst) (to_list_SP (to_rows_SP M ! i)) of None \<Rightarrow> None | Some (i, x) \<Rightarrow> Some x)"
 
 value "retrieveM_SP (identityM_SP 3) 0 1"
-  
+
 value "retrieveM_SP (identityM_SP 3) 1 2"
 value "retrieveM_SP (identityM_SP 3) 0 0"
 value "retrieveM_SP (identityM_SP 3) 1 0"
 value "retrieveM_SP (identityM_SP 3) 2 0"
-  
+
 value "retrieveM_SP (identityM_SP 3) 0 0"
 value "retrieveM_SP (identityM_SP 3) 1 1"
 value "retrieveM_SP (identityM_SP 3) 2 2"
-  
+
 thm filter.simps
 definition to_columns_SP :: "matrix_SP \<Rightarrow> vector_SP list" where
-  "to_columns_SP M \<equiv> (let n = row_size_of_SP M; rows = to_rows_SP M in 
+  "to_columns_SP M \<equiv> (let n = row_size_of_SP M; rows = to_rows_SP M in
      map (\<lambda> j. (n, filter (\<lambda> (i, x). x \<noteq> 0) (map (\<lambda> i. case retrieveV_SP (rows ! i) j of None \<Rightarrow> (i, 0) | Some (_, x) \<Rightarrow> (i, x)) [0..<n]))) [0..<(column_size_of_SP M)]
   )"
 
@@ -606,25 +613,25 @@
 value "to_columns_SP (identityM_SP 3)"
 value "to_columns_SP (insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 0 1) 1 0 1) 2 0 1)"
 
-  
-text "Sparse Matrix Addition." 
-definition addM_SP :: "matrix_SP \<Rightarrow> matrix_SP \<Rightarrow> matrix_SP" where 
+
+text "Sparse Matrix Addition."
+definition addM_SP :: "matrix_SP \<Rightarrow> matrix_SP \<Rightarrow> matrix_SP" where
   "addM_SP M N \<equiv> (let m = column_size_of_SP M; n = row_size_of_SP M in
     (if m = column_size_of_SP N \<and> n = row_size_of_SP N
       then ((m, n), map (\<lambda> (row1, row2). addV_SP row1 row2) (zip (to_rows_SP M) (to_rows_SP N)))
       else undefined))"
-  
+
 value "addM_SP (zeroM_SP 3 3) (zeroM_SP 3 3)"
 value "addM_SP (identityM_SP 3) (identityM_SP 3)"
 
-definition scalarMultM_SP :: "matrix_SP \<Rightarrow> real \<Rightarrow> matrix_SP" where 
+definition scalarMultM_SP :: "matrix_SP \<Rightarrow> real \<Rightarrow> matrix_SP" where
   "scalarMultM_SP M a \<equiv> (let m = column_size_of_SP M; n = row_size_of_SP M in
-    (if 0 = a 
-      then zeroM_SP m n 
+    (if 0 = a
+      then zeroM_SP m n
       else ((m, n), map (\<lambda> row. scalarMultV_SP row a) (to_rows_SP M))
-    ) 
+    )
   )"
-  
+
 value "scalarMultM_SP (identityM_SP 3) 2"
 value "scalarMultM_SP ((3, 2), [(3, [(0, 1), (1, 1), (2, 1)]), (3, [(0, 1), (1, 1), (2, 1)])]) 2"
 
@@ -635,23 +642,23 @@
       else undefined
     )
   )"
-  
+
 value "map (\<lambda> (i, c). scalarProdV_SP (3, [(0, 1), (1, 1), (2, 1)]) c) (zip [0..<3] [(3, [(0, 1)]), (3, [(2, 1)]), (3, [(2, 1)])])"
-  
-definition matrixMultM_SP :: "matrix_SP \<Rightarrow> matrix_SP \<Rightarrow> matrix_SP" where 
+
+definition matrixMultM_SP :: "matrix_SP \<Rightarrow> matrix_SP \<Rightarrow> matrix_SP" where
   "matrixMultM_SP M N \<equiv> (let m = column_size_of_SP M; n = row_size_of_SP N in
     (if m = n
       then (let rows = to_rows_SP M; columns = to_columns_SP N; k = column_size_of_SP M in
         (
-          (row_size_of_SP M, column_size_of_SP N), 
-          map (\<lambda> row. 
+          (row_size_of_SP M, column_size_of_SP N),
+          map (\<lambda> row.
             (k, filter (\<lambda> (i, r). 0 \<noteq> r) (map (\<lambda> (i, column). (i, scalarProdV_SP row column )) (zip [0..<k] columns)))
           ) rows)
         )
       else undefined
     )
   )"
-  
+
 value "matrixMultM_SP (zeroM_SP 3 3) (identityM_SP 3)"
 value "insertM_SP (zeroM_SP 3 3) 1 0 1"
 value "identityM_SP 3"
@@ -662,13 +669,13 @@
 value "(insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 0 1) 1 0 1) 2 0 1)"
 value "(insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 1 1) 0 1 1) 0 2 1)"
 value "matrixMultM_SP (insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 0 1) 1 0 1) 2 0 1) (insertM_SP (insertM_SP (insertM_SP (zeroM_SP 3 3) 0 0 1) 0 1 1) 0 2 1)"
-  
+
+
 
-  
-subsubsection "Invariants"  
-  
+subsubsection "Invariants"
+
 text "Sparse vector invariant: the index list is strictly ascending and no index exceeds or is equal to the stored size."
-definition invarV_SP :: "vector_SP \<Rightarrow> bool" where 
+definition invarV_SP :: "vector_SP \<Rightarrow> bool" where
   "invarV_SP v \<equiv> (let indexes = indexesLV_SP (to_list_SP v); size = size_of_SP v in
     strictly_ascending indexes & (\<forall>i\<in>set indexes. i < size)
   )"
@@ -677,25 +684,25 @@
 definition invarM_SP :: "matrix_SP \<Rightarrow> bool" where
   "invarM_SP M \<equiv> (length (to_rows_SP M) = row_size_of_SP M & (\<forall> v \<in> set (to_rows_SP M). size_of_SP v = column_size_of_SP M & invarV_SP v))"
 
-  
-  
+
+
 subsection "Proofs"
 
- 
-lemma "invarV_LIL v \<Longrightarrow> sorted [0..<size_of v]" 
+
+lemma "invarV_LIL v \<Longrightarrow> sorted [0..<size_of v]"
   by simp
 lemma "invarV_LIL v \<Longrightarrow> sorted [0..<size_of v] \<Longrightarrow> sorted (map fst (zip [0..<size_of v] (to_list v)))"
   apply(induction "to_list v")
   apply(auto)
-  subgoal sledgehammer
+  subgoal
     by (simp add: invarV_LIL_def)
   done
-    
+
 lemma[simp]: "invarV_LIL v \<Longrightarrow> sorted [0..<size_of v] \<Longrightarrow> sorted (map fst (zip [0..<size_of v] (to_list v))) \<Longrightarrow> sorted  (map fst  (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v))))"
-  using sorted_filter 
+  using sorted_filter
   by blast
-    
-lemma "invarV_LIL v \<Longrightarrow> distinct [0..<size_of v]" 
+
+lemma "invarV_LIL v \<Longrightarrow> distinct [0..<size_of v]"
   by simp
 lemma "invarV_LIL v \<Longrightarrow> distinct [0..<size_of v] \<Longrightarrow> distinct (map fst (zip [0..<size_of v] (to_list v)))"
   apply(induction "to_list v")
@@ -704,10 +711,10 @@
    by (simp add: invarV_LIL_def)
   done
 lemma[simp]:"invarV_LIL v \<Longrightarrow> distinct [0..<size_of v] \<Longrightarrow> distinct (map fst (zip [0..<size_of v] (to_list v))) \<Longrightarrow> distinct (map fst  (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v))))"
-  using distinct_map_filter 
+  using distinct_map_filter
   by blast
-  
-lemma condense_preserves_vector_invar_aux_1: 
+
+lemma condense_preserves_vector_invar_aux_1:
   assumes "invarV_LIL v"
   shows "strictly_ascending (indexesLV_SP (to_list_SP (condenseV v)))"
 proof -
@@ -715,108 +722,108 @@
     by blast
   have "indexesLV_SP (to_list_SP (condenseV v)) = indexesLV_SP (to_list_SP ((k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))))"
     by (metis \<open>k = size_of v\<close> \<open>l = to_list v\<close> condenseV_def)
-  also have "\<dots> = indexesLV_SP (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))" 
-    using to_list_SP_def 
+  also have "\<dots> = indexesLV_SP (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))"
+    using to_list_SP_def
     by auto
-  also have "\<dots> = (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))" 
-    using indexesLV_SP_def 
-    by blast 
-  hence "strictly_ascending (indexesLV_SP (to_list_SP (condenseV v))) = strictly_ascending (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))" 
+  also have "\<dots> = (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
+    using indexesLV_SP_def
+    by blast
+  hence "strictly_ascending (indexesLV_SP (to_list_SP (condenseV v))) = strictly_ascending (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
     by (simp add: calculation)
   hence "strictly_ascending (indexesLV_SP (to_list_SP (condenseV v))) = sorted (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) & distinct (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
-    by (metis (no_types, lifting) \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms diff_zero distinct_map_filter distinct_upt invarV_LIL_def length_upt map_fst_zip strictly_ascending_def) 
+    by (metis (no_types, lifting) \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms diff_zero distinct_map_filter distinct_upt invarV_LIL_def length_upt map_fst_zip strictly_ascending_def)
   thus ?thesis
-    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms invarV_LIL_def 
+    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms invarV_LIL_def
     by auto
 qed
 
-lemma condense_preserves_vector_invar_aux_2_1: 
+lemma condense_preserves_vector_invar_aux_2_1:
   "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) = fst ` set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
   by simp
-    
-lemma condense_preserves_vector_invar_aux_2_2: "(set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> set (zip [0..<k] l)" 
+
+lemma condense_preserves_vector_invar_aux_2_2: "(set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> set (zip [0..<k] l)"
   by auto
-    
+
 lemma condense_preserves_vector_invar_aux_2_3: "fst ` set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)) \<subseteq> fst ` set (zip [0..<k] l)"
     using condense_preserves_vector_invar_aux_2_2
     by blast
-      
-lemma condense_preserves_vector_invar_aux_2_4: 
+
+lemma condense_preserves_vector_invar_aux_2_4:
   assumes "invarV_LIL v"
   shows "fst ` set (zip [0..<size_of v] (to_list v)) = set [0..<size_of v]"
   by (metis assms diff_zero invarV_LIL_def length_upt map_fst_zip set_map)
 
-lemma condense_preserves_vector_invar_aux_2: 
+lemma condense_preserves_vector_invar_aux_2:
   assumes "invarV_LIL v"
   shows "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v))))) \<subseteq> (set [0..<size_of v])"
 proof -
-  obtain k l where "k = size_of v" and "l = to_list v" 
-    by blast 
-  have "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) = fst ` set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))" 
+  obtain k l where "k = size_of v" and "l = to_list v"
+    by blast
+  have "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) = fst ` set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
     by simp
-  hence "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> fst ` set (zip [0..<k] l))" 
+  hence "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> fst ` set (zip [0..<k] l))"
     using condense_preserves_vector_invar_aux_2_1 condense_preserves_vector_invar_aux_2_2
     by blast
   hence "(set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))) \<subseteq> (set [0..<k])"
     using condense_preserves_vector_invar_aux_2_4
-    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms 
+    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms
     by blast
   thus ?thesis
-    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> 
-  by blast 
+    using \<open>k = size_of v\<close> \<open>l = to_list v\<close>
+  by blast
 qed
-    
-lemma condense_preserves_vector_invar_aux_3: 
+
+lemma condense_preserves_vector_invar_aux_3:
   assumes "invarV_LIL v"
   shows "set (indexesLV_SP (to_list_SP (condenseV v))) \<subseteq> set ([0..<size_of_SP (condenseV v)])"
 proof -
-  obtain k l where "k = size_of v" and "l = to_list v" 
+  obtain k l where "k = size_of v" and "l = to_list v"
     by blast
    have A: "set ([0..<size_of_SP (condenseV v)]) = set ([0..<k])"
      by (metis \<open>k = size_of v\<close> condenseV_def fst_conv size_of_SP_def)
-  have B: "set (indexesLV_SP (to_list_SP (condenseV v))) = set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))" 
+  have B: "set (indexesLV_SP (to_list_SP (condenseV v))) = set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l)))"
     by (metis \<open>k = size_of v\<close> \<open>l = to_list v\<close> condenseV_def indexesLV_SP_def snd_conv to_list_SP_def)
-  hence "(set (indexesLV_SP (to_list_SP (condenseV v))) \<subseteq> set ([0..<size_of_SP (condenseV v)])) = (set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> set ([0..<k]))" 
-    using A 
-    by blast 
+  hence "(set (indexesLV_SP (to_list_SP (condenseV v))) \<subseteq> set ([0..<size_of_SP (condenseV v)])) = (set (map fst (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))) \<subseteq> set ([0..<k]))"
+    using A
+    by blast
   thus ?thesis
-    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms condense_preserves_vector_invar_aux_2 
+    using \<open>k = size_of v\<close> \<open>l = to_list v\<close> assms condense_preserves_vector_invar_aux_2
     by blast
 qed
 
-lemma condense_preserves_vector_invar_aux_4: 
+lemma condense_preserves_vector_invar_aux_4:
   assumes "invarV_LIL v"
   shows "\<forall>i\<in>set (indexesLV_SP (to_list_SP (condenseV v))). i < size_of_SP (condenseV v)"
 proof -
   fix i
   have "i\<in>set (indexesLV_SP (to_list_SP (condenseV v))) \<Longrightarrow> i \<in> set ([0..<size_of_SP (condenseV v)])"
-    using assms condense_preserves_vector_invar_aux_3 
-    by blast 
-  hence "i\<in>set (indexesLV_SP (to_list_SP (condenseV v))) \<Longrightarrow> i < size_of_SP (condenseV v)" 
-    using atLeast_upt 
-    by blast       
+    using assms condense_preserves_vector_invar_aux_3
+    by blast
+  hence "i\<in>set (indexesLV_SP (to_list_SP (condenseV v))) \<Longrightarrow> i < size_of_SP (condenseV v)"
+    using atLeast_upt
+    by blast
   thus ?thesis
-    using condense_preserves_vector_invar_aux_3 assms atLeast_upt 
+    using condense_preserves_vector_invar_aux_3 assms atLeast_upt
     by blast
 qed
-    
-lemma condense_preserves_vector_invar: 
+
+lemma condense_preserves_vector_invar:
   assumes "invarV_LIL v"
   shows "invarV_SP (condenseV v)"
 proof -
   have A: "invarV_LIL v \<Longrightarrow> strictly_ascending (indexesLV_SP (to_list_SP (condenseV v)))"
     by (simp add: condense_preserves_vector_invar_aux_1)
   have B: "invarV_LIL v \<Longrightarrow> \<forall>i\<in>set (indexesLV_SP (to_list_SP (condenseV v))). i < size_of_SP (condenseV v)"
-    using condense_preserves_vector_invar_aux_4 
+    using condense_preserves_vector_invar_aux_4
     by blast
-  thus ?thesis using assms A B 
+  thus ?thesis using assms A B
     by (simp add: invarV_SP_def)
 qed
-    
+
 lemma[simp]:
   assumes "invarM_LIL M"
   shows "\<forall>v\<in>set(to_rows M). invarV_LIL v"
-proof - 
+proof -
   fix v
   have "v\<in>set(to_rows M) \<Longrightarrow> invarV_LIL v" using invarM_LIL_def
     by (meson assms)
@@ -833,60 +840,60 @@
   fix x
     have "x\<in>(set (to_rows M)) \<Longrightarrow> invarV_LIL x"
       by (meson assms(1) invarM_LIL_def)
-    hence "x\<in>(set (to_rows M)) \<Longrightarrow> invarV_SP (condenseV x)" 
-      using condense_preserves_vector_invar 
+    hence "x\<in>(set (to_rows M)) \<Longrightarrow> invarV_SP (condenseV x)"
+      using condense_preserves_vector_invar
       by simp
   thus ?thesis
-    using assms(1) assms(3) condense_preserves_vector_invar 
+    using assms(1) assms(3) condense_preserves_vector_invar
     by force
 qed
-  
-lemma condense_preserves_matrix_invar_aux2: 
+
+lemma condense_preserves_matrix_invar_aux2:
   assumes "invarM_LIL M"
   shows "\<forall>v\<in>set(map condenseV (to_rows M)). invarV_SP v"
 proof -
   fix v
-  have "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>condenseV ` (set (to_rows M))" 
+  have "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>condenseV ` (set (to_rows M))"
     by auto
-  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>{y. \<exists>x\<in>(set (to_rows M)). y = condenseV x}" 
-    using Set.image_def 
-    by blast 
-  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x)" 
-    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> v \<in> {y. \<exists>x\<in>set (to_rows M). y = condenseV x}\<close> 
+  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>{y. \<exists>x\<in>(set (to_rows M)). y = condenseV x}"
+    using Set.image_def
     by blast
-  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x) \<Longrightarrow> invarV_SP v" 
-    using assms condense_preserves_matrix_invar_aux1 
+  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x)"
+    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> v \<in> {y. \<exists>x\<in>set (to_rows M). y = condenseV x}\<close>
+    by blast
+  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x) \<Longrightarrow> invarV_SP v"
+    using assms condense_preserves_matrix_invar_aux1
     by blast
   thus ?thesis
-    using assms condense_preserves_vector_invar 
+    using assms condense_preserves_vector_invar
     by force
-qed  
-  
-lemma condense_preserves_matrix_invar_aux3: 
+qed
+
+lemma condense_preserves_matrix_invar_aux3:
   assumes "invarM_LIL M"
   assumes "v\<in>set(map condenseV (to_rows M))"
   shows "size_of_SP v = column_size_of M"
 proof -
-  have "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>condenseV ` (set (to_rows M))" 
+  have "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>condenseV ` (set (to_rows M))"
     by auto
-  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>{y. \<exists>x\<in>(set (to_rows M)). y = condenseV x}" 
-    using Set.image_def 
-    by blast 
-hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x)" 
-    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> v \<in> {y. \<exists>x\<in>set (to_rows M). y = condenseV x}\<close> 
+  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> v\<in>{y. \<exists>x\<in>(set (to_rows M)). y = condenseV x}"
+    using Set.image_def
     by blast
-  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x) \<Longrightarrow> size_of_SP v = column_size_of M" 
-    by (metis assms(1) condenseV_def fst_conv invarM_LIL_def size_of_SP_def) 
+hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x)"
+    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> v \<in> {y. \<exists>x\<in>set (to_rows M). y = condenseV x}\<close>
+    by blast
+  hence "v\<in>set(map condenseV (to_rows M)) \<Longrightarrow> (\<exists>x\<in>(set (to_rows M)). v = condenseV x) \<Longrightarrow> size_of_SP v = column_size_of M"
+    by (metis assms(1) condenseV_def fst_conv invarM_LIL_def size_of_SP_def)
   thus ?thesis
-    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> \<exists>x\<in>set (to_rows M). v = condenseV x\<close> assms(2) 
+    using \<open>v \<in> set (map condenseV (to_rows M)) \<Longrightarrow> \<exists>x\<in>set (to_rows M). v = condenseV x\<close> assms(2)
     by blast
 qed
- 
+
 lemma condense_preserves_matrix_invar_aux4:
   assumes "invarM_LIL M"
   shows "length (to_rows_SP (condenseM M)) = row_size_of M"
   by (metis assms condenseM_def invarM_LIL_def length_map snd_conv to_rows_SP_def)
-  
+
 lemma condense_preserves_matrix_invar_aux5:
   assumes "invarM_LIL M"
   shows "invarM_SP (condenseM M) = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = (column_size_of M) & invarV_SP v))"
@@ -897,12 +904,12 @@
     using calculation invarM_SP_def
     by blast
   also have "\<dots> = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (to_rows_SP (condenseM M)). size_of_SP v = column_size_of_SP (condenseM M) & invarV_SP v))"
-    using condenseM_def row_size_of_SP_def 
-    by auto 
+    using condenseM_def row_size_of_SP_def
+    by auto
   also have "\<dots> = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (to_rows_SP ((column_size_of M,  row_size_of M), map condenseV (to_rows M))). size_of_SP v = column_size_of_SP (condenseM M) & invarV_SP v))"
-    using condenseM_def to_rows_SP_def 
-    by auto 
-  also have "\<dots> = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = column_size_of_SP (condenseM M) & invarV_SP v))" 
+    using condenseM_def to_rows_SP_def
+    by auto
+  also have "\<dots> = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = column_size_of_SP (condenseM M) & invarV_SP v))"
     by (simp add: to_rows_SP_def)
   finally have "\<dots> = (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = (column_size_of M) & invarV_SP v))"
     by (simp add: column_size_of_SP_def condenseM_def)
@@ -911,7 +918,7 @@
 qed
 
 text "Show that condensation of a LIL matrix conforming to the LIL matrix invariant produces a sparse Matrix which conforms to the sparse matrix invariant."
-lemma condense_preserves_matrix_invar: 
+lemma condense_preserves_matrix_invar:
   assumes "invarM_LIL M"
     shows "invarM_SP (condenseM M)"
 proof -
@@ -920,11 +927,11 @@
     by blast
   hence "invarM_LIL M \<Longrightarrow> (length (to_rows_SP (condenseM M)) = (row_size_of M) & (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = (column_size_of M) & invarV_SP v))"
     by (simp add: condense_preserves_matrix_invar_aux2 condense_preserves_matrix_invar_aux3 condense_preserves_matrix_invar_aux4)
-  thus ?thesis 
-    using \<open>invarM_SP (condenseM M) = (length (to_rows_SP (condenseM M)) = row_size_of M \<and> (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = column_size_of M \<and> invarV_SP v))\<close> assms 
+  thus ?thesis
+    using \<open>invarM_SP (condenseM M) = (length (to_rows_SP (condenseM M)) = row_size_of M \<and> (\<forall>v\<in>set (map condenseV (to_rows M)). size_of_SP v = column_size_of M \<and> invarV_SP v))\<close> assms
     by blast
 qed
-    
+
 lemma [simp]: "k = length l \<Longrightarrow> (\<forall> (i, x) \<in> set (zip [0..<k] l). x = (l ! i))"
 proof -
   consider (A) "k = 0"
@@ -932,39 +939,39 @@
     by blast
   then show ?thesis proof (cases)
     case A
-    then show ?thesis 
+    then show ?thesis
       by simp
   next
     case B
     then show ?thesis proof -
-      have "zip [0..<length l] l = map (\<lambda> i. (i, l ! i)) [0..<length l]" 
+      have "zip [0..<length l] l = map (\<lambda> i. (i, l ! i)) [0..<length l]"
         by (metis add.left_neutral enumerate_eq_zip enumerate_map_upt map_nth)
       hence "set (zip [0..<length l] l) = set (map (\<lambda> i. (i, l ! i)) [0..<length l])"
         by simp
-      hence "\<forall> (i, x) \<in> set (zip [0..<length l] l). x = l ! i" 
+      hence "\<forall> (i, x) \<in> set (zip [0..<length l] l). x = l ! i"
         by simp
       thus ?thesis
         by (metis (no_types, lifting) add.left_neutral diff_zero in_set_zip length_upt nth_upt)
     qed
   qed
 qed
-  
+
 lemma condenseV_set_aux: "\<forall> (i, x) \<in> Set.filter (\<lambda> (i, x). x \<noteq> 0) (set (zip [0..<(length l)] l)). x \<noteq> 0 & x = (l ! i)"
   by (smt map_nth mem_Collect_eq member_filter min_less_iff_conj nth_map prod.simps(2) set_zip)
 
 lemma condenseV_set_aux2: "\<forall> (i, x) \<in> set (zip [0..<size_of v] (to_list v)). i\<in>set [0..<size_of v]"
   apply(induction "to_list v")
   apply(auto)
-  subgoal 
-    using set_zip_leftD 
+  subgoal
+    using set_zip_leftD
     by fastforce
   done
-    
+
 corollary [simp]: "\<forall> (i, x) \<in> set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v))). i\<in>set [0..<size_of v]"
   apply(induction "to_list v")
   apply(auto)
-  subgoal 
-    using set_zip_leftD 
+  subgoal
+    using set_zip_leftD
     by fastforce
   done
 
@@ -974,24 +981,24 @@
   have "(i, x) \<in> set (to_list_SP (condenseV v)) \<Longrightarrow> (i, x) \<in> set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v)))"
     by (metis condenseV_def snd_conv to_list_SP_def)
   hence "(i, x) \<in> set (to_list_SP (condenseV v)) \<Longrightarrow> i \<in> set [0..<size_of v]"
-    by (metis filter_set in_set_zipE member_filter) 
+    by (metis filter_set in_set_zipE member_filter)
   thus ?thesis
     by (metis atLeast_upt case_prodI2 condenseV_def eq_snd_iff filter_set lessThan_iff member_filter nat_le_linear not_le set_zip_leftD to_list_SP_def)
 qed
-    
+
 lemma condenseV_set_aux4: "x = (to_list v ! i) & i < (size_of v) \<Longrightarrow> Some x = retrieveV_LIL v i"
   by (simp add: retrieveV_LIL_def)
-    
+
 lemma condenseV_set:
   assumes "invarV v"
   shows "\<forall> (i,x)\<in>set (to_list_SP (condenseV v)). x \<noteq> 0 & x = (to_list v ! i)"
 proof -
   obtain k where "k = size_of v"
     by simp
-  have "condenseV v = (k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] (to_list v)))" 
+  have "condenseV v = (k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] (to_list v)))"
     by (metis \<open>k = size_of v\<close> condenseV_def)
-  hence "set (to_list_SP (condenseV v)) = set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] (to_list v)))" 
-    using to_list_SP_def 
+  hence "set (to_list_SP (condenseV v)) = set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] (to_list v)))"
+    using to_list_SP_def
     by auto
   hence "set (to_list_SP (condenseV v)) = Set.filter (\<lambda> (i, x). x \<noteq> 0) (set (zip [0..<k] (to_list v)))"
     by (simp add: filter_set)
@@ -1002,43 +1009,43 @@
   hence "\<forall> (i, x) \<in> set (to_list_SP (condenseV v)). x\<noteq>0 & x = (to_list v ! i)"
     using condenseV_set_aux[of "to_list v"]
     by (metis (no_types, lifting) add.left_neutral diff_zero in_set_zip length_upt member_filter nth_upt)
-  thus ?thesis 
+  thus ?thesis
     by blast
 qed
-  
+
 text "Condensation of a LIL vector `v` conforming to the invariant results in eliminations of zeros and preservation of ordering: i.e. for every pair `(i, x)` of the condensated vector, it holds that `x = 0` and `x` is the element at index `i` of `v`."
 corollary
-  assumes "invarV v" 
+  assumes "invarV v"
   shows "\<forall> (i,x)\<in>set (to_list_SP (condenseV v)). x \<noteq> 0 & Some x = retrieveV_LIL v i"
 proof -
   have "\<forall> (i, x)\<in>set (to_list_SP (condenseV v)). x \<noteq> 0 & x = (to_list v ! i)"
-    using condenseV_set 
+    using condenseV_set
     by simp
-  thus ?thesis 
-    by (smt atLeastLessThan_iff case_prodI2 condenseV_def condenseV_set_aux4 filter_set fst_conv in_set_zipE member_filter prod.case_eq_if set_upt snd_conv to_list_SP_def) 
+  thus ?thesis
+    by (smt atLeastLessThan_iff case_prodI2 condenseV_def condenseV_set_aux4 filter_set fst_conv in_set_zipE member_filter prod.case_eq_if set_upt snd_conv to_list_SP_def)
 qed
 
 (*unfinished:
 lemma sparseV_covers_non_zero_set:
   assumes "invarV v"
   assumes "v' = condenseV v"
-  assumes "i \<in> set [0..<size_of v]" 
+  assumes "i \<in> set [0..<size_of v]"
   assumes "x = (to_list v) ! i"
   shows "\<exists> (i', x') \<in> set(to_list_SP v'). (x' = x) & (i' = i)"
 proof -
   obtain k l where "k = size_of v" and "l = to_list v"
-    by simp  
-  have "condenseV v = (k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))" 
+    by simp
+  have "condenseV v = (k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))"
     by (metis \<open>k = size_of v\<close> \<open>l = to_list v\<close> condenseV_def)
-  hence "set (to_list_SP v') = set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))" 
+  hence "set (to_list_SP v') = set (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))"
     by (simp add: assms(2) to_list_SP_def)
   hence "set (to_list_SP v') = Set.filter (\<lambda> (i, x). x \<noteq> 0) (set (zip [0..<k] l))"
     by (simp add: filter_set)
   thus ?thesis sorry
       oops
 qed
-  
-lemma sparseV_does_not_contain_zero: 
+
+lemma sparseV_does_not_contain_zero:
   assumes "invarV v"
   assumes "v' = condenseV v"
   shows "\<forall> (i, x) \<in> set (to_list_SP v'). x \<noteq> 0"
@@ -1046,27 +1053,27 @@
   -- " (k, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<k] l))"
   fix i x
     obtain i x where "(i, x) \<in> set (to_list_SP v')" sledgehammer
-    
+
 
 lemma condenseV_preserves_non_zero_elements_and_index:
   assumes "invarV_LIL v"
-  shows "\<forall>i \<in> set [0..<size_of v]. (i, (to_list v ! i)) \<in> set (to_list_SP (condenseV v)) | 0 = (to_list v ! i)" 
+  shows "\<forall>i \<in> set [0..<size_of v]. (i, (to_list v ! i)) \<in> set (to_list_SP (condenseV v)) | 0 = (to_list v ! i)"
 proof -
   consider (A) "size_of v = 0"
     | (B) "size_of v > 0"
     by blast
   then show ?thesis proof (cases)
     case A
-    have "set [0..<0] = {}" 
+    have "set [0..<0] = {}"
       by simp
-    thus ?thesis by (simp add: A) 
+    thus ?thesis by (simp add: A)
   next case B
     fix i
     obtain i where "i\<in> set[0..<size_of v]"
-      using B 
+      using B
       by auto
-    obtain x where "(i, x) = (i, to_list v ! i)" 
-      by simp  
+    obtain x where "(i, x) = (i, to_list v ! i)"
+      by simp
     consider (B1) "x = 0"
       | (B2) "x \<noteq> 0"
       by blast
@@ -1079,7 +1086,7 @@
       qed
   qed
 qed
-  
+
 lemma condenseV_eliminates_zeros:
   assumes "v' = condenseV v"
   assumes "i \<in> set [0..<size_of v]"
@@ -1089,72 +1096,72 @@
   show ?thesis sorry
 qed
 *)
-  
+
 lemma condenseM_preserves_row_size: "invarM M \<Longrightarrow> length (to_rows M) = length (to_rows_SP (condenseM M))"
 proof -
   have "length (to_rows_SP (condenseM M)) = length (to_rows_SP ((m, n), map condenseV (to_rows M)))"
     by (simp add: condenseM_def to_rows_SP_def)
-  also have "\<dots> = length (map condenseV (to_rows M))" 
+  also have "\<dots> = length (map condenseV (to_rows M))"
     by (simp add: to_rows_SP_def)
   also have "\<dots> = length (to_rows M)"
     by simp
   thus ?thesis
     by (simp add: calculation)
 qed
-  
+
 lemma [simp]: "\<forall>i\<in>set [0..<length l]. i \<le> length l"
   apply(induction l)
   apply(auto)
   done
 
-corollary[simp]: 
+corollary[simp]:
   assumes "invarM_LIL M"
   assumes "i\<in>set [0..<row_size_of M]"
   shows "i < length (to_rows M)"
 proof (rule ccontr)
   assume A: "\<not>?thesis"
   then show False proof -
-    from A have "\<not>(i < length (to_rows M))" 
+    from A have "\<not>(i < length (to_rows M))"
       by auto
-    hence "i \<notin> set [0..<(length (to_rows M))]" 
+    hence "i \<notin> set [0..<(length (to_rows M))]"
       by (simp add: A)
-    hence "i \<notin> set [0..<(row_size_of M)]" 
-      using assms(1) invarM_LIL_def 
+    hence "i \<notin> set [0..<(row_size_of M)]"
+      using assms(1) invarM_LIL_def
         by metis
-    thus False 
-      using assms(2) 
+    thus False
+      using assms(2)
       by auto
   qed
 qed
-      
+
 text "Condensation returns condensed vectors in the order which they were found in the original matrix."
 lemma condenseM_preserves_row_ordering:
-  assumes "invarM_LIL M" 
+  assumes "invarM_LIL M"
   assumes "i\<in> set [0..<row_size_of M]"
   shows "to_rows_SP (condenseM M) ! i = condenseV (to_rows M ! i)"
 proof -
-  have "i\<in> set [0..<row_size_of M] \<Longrightarrow> i < row_size_of M" 
+  have "i\<in> set [0..<row_size_of M] \<Longrightarrow> i < row_size_of M"
     by simp
-  from this have B: "i\<in> set [0..<row_size_of M] \<Longrightarrow> i < length (to_rows M)" 
-    using assms 
+  from this have B: "i\<in> set [0..<row_size_of M] \<Longrightarrow> i < length (to_rows M)"
+    using assms
     by auto
-  have "to_rows_SP (condenseM M) ! i = to_rows_SP (((m, n), map condenseV (to_rows M))) ! i" 
+  have "to_rows_SP (condenseM M) ! i = to_rows_SP (((m, n), map condenseV (to_rows M))) ! i"
     by (simp add: condenseM_def to_rows_SP_def)
-  also have "\<dots> = map condenseV (to_rows M) ! i" 
-    using to_rows_SP_def 
+  also have "\<dots> = map condenseV (to_rows M) ! i"
+    using to_rows_SP_def
     by simp
-  finally have "\<dots> = condenseV (to_rows M ! i)" 
+  finally have "\<dots> = condenseV (to_rows M ! i)"
     using assms(2) and B and nth_map[of i "(to_rows M)" "condenseV"]
     by blast
-  thus ?thesis 
+  thus ?thesis
     by (simp add: \<open>to_rows_SP ((m, n), map condenseV (to_rows M)) ! i = map condenseV (to_rows M) ! i\<close> \<open>to_rows_SP (condenseM M) ! i = to_rows_SP ((m, n), map condenseV (to_rows M)) ! i\<close>)
 qed
 
-  
-  
+
+
 (*
  * III. Equivalence of LIL Matrix and Sparse Matrix operations.
- *)  
+ *)
 section "Equivalence of LIL Matrix and Sparse Matrix Operations"
 subsection "Vector Addition"
 
@@ -1168,12 +1175,12 @@
 have "condenseV (addV_LIL v w) = condenseV (size_of v, map (\<lambda> (a, b). a + b) (zip (to_list v) (to_list w)))"
     by (simp add: addV_LIL_def assms(3))
   also have "\<dots> = (size_of v, filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (map (\<lambda> (a, b). a + b) (zip (to_list v) (to_list w)))))"
-    using condenseV_def 
+    using condenseV_def
     by force
   thus ?thesis
     by (simp add: calculation)
 oops
-  
+
 lemma condense_preserves_vector_addition_aux2:
   assumes "invarV_LIL v"
   assumes "invarV_LIL w"
@@ -1187,10 +1194,10 @@
   also have "\<dots> = (size_of v, addV_SP' (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of v] (to_list v))) (filter (\<lambda> (i, x). x \<noteq> 0) (zip [0..<size_of w] (to_list w))))"
     using to_list_SP_def
     by simp
-  thus ?thesis 
+  thus ?thesis
   by (simp add: calculation)
 qed
-    
+
 lemma condense_preserves_vector_addition_aux3:
   assumes "invarV_LIL v"
   assumes "invarV_LIL w"
@@ -1206,9 +1213,9 @@
   assumes "size_of v = size_of w"
   shows "condenseV (addV_LIL v w) = addV_SP (condenseV v) (condenseV w)" sorry
 
-  
-  
-  
+
+
+
 subsection "Matrix Addition"
 
 lemma condense_preserves_matrix_addition_aux1:
@@ -1221,20 +1228,20 @@
   obtain m1 m2 n1 n2 where "m1 = column_size_of M" and "n1 = row_size_of M" and "m2 = column_size_of N" and "n2 = row_size_of N"
     by blast
   have "condenseM (addM_LIL M N) = condenseM ((m1, n1), map (\<lambda> (v, w). addV_LIL v w) (zip (to_rows M) (to_rows N)))"
-    using \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> addM_LIL_def assms(3) assms(4) 
+    using \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> addM_LIL_def assms(3) assms(4)
     by auto
-  also have "\<dots> = ((m1, n1), map condenseV (map (\<lambda> (v, w). addV_LIL v w) (zip (to_rows M) (to_rows N))))" 
-    using condenseM_def 
+  also have "\<dots> = ((m1, n1), map condenseV (map (\<lambda> (v, w). addV_LIL v w) (zip (to_rows M) (to_rows N))))"
+    using condenseM_def
     by simp
   also have "\<dots> = ((m1, n1), map (condenseV \<circ> (\<lambda> (v, w). addV_LIL v w)) (zip (to_rows M) (to_rows N)))"
-    using List.map_map 
+    using List.map_map
     by simp
   also have "\<dots> = ((m1, n1), map (\<lambda> (v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N)))"
     by auto
   thus ?thesis
     by (simp add: \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> calculation)
 qed
-  
+
 lemma condense_preserves_matrix_addition_aux2:
   assumes "invarM M"
   assumes "invarM N"
@@ -1247,32 +1254,32 @@
   have "addM_SP (condenseM M) (condenseM N) = addM_SP ((m1, n1), map condenseV (to_rows M)) ((m2, n2), map condenseV (to_rows N))"
     by (simp add: \<open>m1 = column_size_of M\<close> \<open>m2 = column_size_of N\<close> \<open>n1 = row_size_of M\<close> \<open>n2 = row_size_of N\<close> condenseM_def)
   also have "\<dots> = ((m1, n1), map (\<lambda> (row1, row2). addV_SP row1 row2) (zip (map condenseV (to_rows M)) (map condenseV (to_rows N))))"
-    using \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> addM_SP_def assms(3) assms(4) calculation column_size_of_SP_def condenseM_def row_size_of_SP_def to_rows_SP_def 
+    using \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> addM_SP_def assms(3) assms(4) calculation column_size_of_SP_def condenseM_def row_size_of_SP_def to_rows_SP_def
     by auto
   also have "\<dots> = ((m1, n1), map (\<lambda> (row1, row2). addV_SP row1 row2) (map (\<lambda> (v, w). (condenseV v, condenseV w)) (zip (to_rows M) (to_rows N))))"
     by (simp add: zip_map_map)
   also have "\<dots> = ((m1, n1), map ((\<lambda> (row1, row2). addV_SP row1 row2) \<circ> (\<lambda> (v, w). (condenseV v, condenseV w))) (zip (to_rows M) (to_rows N)))"
-    by simp 
+    by simp
   also have "\<dots> = ((m1, n1), map (\<lambda> (row1, row2). addV_SP (condenseV row1) (condenseV row2)) (zip (to_rows M) (to_rows N)))"
     by auto
   thus ?thesis
     by (simp add: \<open>m1 = column_size_of M\<close> \<open>n1 = row_size_of M\<close> calculation)
 qed
-  
+
 lemma condense_preserves_matrix_addition_aux3:
   assumes "invarM_LIL M"
   assumes "invarM_LIL N"
   assumes "row_size_of M = row_size_of N"
   assumes "column_size_of M = column_size_of N"
-  shows "\<forall>(v, w)\<in>set (zip (to_rows M) (to_rows N)). invarV_LIL v & invarV_LIL w" 
+  shows "\<forall>(v, w)\<in>set (zip (to_rows M) (to_rows N)). invarV_LIL v & invarV_LIL w"
 proof -
-  fix v w 
+  fix v w
   have "(v, w) \<in>set (zip (to_rows M) (to_rows N)) \<Longrightarrow> v \<in> set (to_rows M) & w \<in> set (to_rows N)"
-    by (meson in_set_zipE) 
+    by (meson in_set_zipE)
   thus ?thesis using assms
     by (metis (no_types, lifting) case_prodI2 invarM_LIL_def set_zip_leftD set_zip_rightD)
 qed
-  
+
 lemma condense_preserves_matrix_addition_aux4:
   assumes "invarM_LIL M"
   assumes "invarM_LIL N"
@@ -1280,17 +1287,17 @@
   assumes "column_size_of M = column_size_of N"
   shows "\<forall>(v, w)\<in>set (zip (to_rows M) (to_rows N)). (condenseV (addV_LIL v w)) = addV_SP (condenseV v) (condenseV w)"
 proof -
-  fix v w 
+  fix v w
   have A: "(v, w)\<in>set (zip (to_rows M) (to_rows N)) \<Longrightarrow> invarV_LIL v & invarV_LIL w"
     by (meson assms(1) assms(2) invarM_LIL_def set_zip_leftD set_zip_rightD)
   have B: "(v, w)\<in>set (zip (to_rows M) (to_rows N)) \<Longrightarrow> size_of v = size_of w"
-    by (metis assms(1) assms(2) assms(4) invarM_LIL_def set_zip_leftD set_zip_rightD) 
+    by (metis assms(1) assms(2) assms(4) invarM_LIL_def set_zip_leftD set_zip_rightD)
   have C: "(v, w)\<in>set (zip (to_rows M) (to_rows N)) \<Longrightarrow> condenseV (addV_LIL v w) = addV_SP (condenseV v) (condenseV w)"
     using A B condense_preserves_vector_addition by blast
   thus ?thesis
     by (smt assms(1) assms(2) assms(4) case_prodI2 condense_preserves_vector_addition invarM_LIL_def set_zip_leftD set_zip_rightD)
 qed
-  
+
 lemma condense_preserves_matrix_addition_aux5:
   assumes "invarM_LIL M"
   assumes "invarM_LIL N"
@@ -1299,22 +1306,22 @@
   shows "map (\<lambda> (v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N)) = map (\<lambda> (v, w). (addV_SP (condenseV v) (condenseV w))) (zip (to_rows M) (to_rows N))"
 proof -
   have  "\<forall>(v, w)\<in>set (zip (to_rows M) (to_rows N)). (condenseV (addV_LIL v w)) = addV_SP (condenseV v) (condenseV w)"
-    using assms condense_preserves_matrix_addition_aux4 
+    using assms condense_preserves_matrix_addition_aux4
     by blast
   thus ?thesis
     by auto
 qed
-    
+
 text "Condensing the result of a LIL matrix addition yields the same result as condensing the matrices and adding the condensed matrices: i.e. sparse matrix addition is correct given that LIL matrix addition is correct."
 lemma condense_preserves_matrix_addition:
   assumes "invarM_LIL M"
   assumes "invarM_LIL N"
   assumes "row_size_of M = row_size_of N"
   assumes "column_size_of M = column_size_of N"
-  shows "condenseM (addM_LIL M N) = addM_SP (condenseM M) (condenseM N)" 
+  shows "condenseM (addM_LIL M N) = addM_SP (condenseM M) (condenseM N)"
 proof -
   have "condenseM (addM_LIL M N) = ((column_size_of M, row_size_of M), map (\<lambda> (v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N)))"
-    using assms(3) assms(4) condense_preserves_matrix_addition_aux1 
+    using assms(3) assms(4) condense_preserves_matrix_addition_aux1
     by blast
   also have "\<dots> = ((column_size_of M, row_size_of M), map (\<lambda> (v, w). (addV_SP (condenseV v) (condenseV w))) (zip (to_rows M) (to_rows N)))"
     using assms(1) assms(2) assms(3) assms(4) condense_preserves_matrix_addition_aux5
@@ -1322,11 +1329,11 @@
   also have "\<dots> = ((column_size_of M, row_size_of M), map (\<lambda> (row1, row2). addV_SP (condenseV row1) (condenseV row2)) (zip (to_rows M) (to_rows N)))"
     by blast
   finally have " \<dots> = addM_SP (condenseM M) (condenseM N)"
-    using assms(3) assms(4) condense_preserves_matrix_addition_aux2 
+    using assms(3) assms(4) condense_preserves_matrix_addition_aux2
     by auto
   thus ?thesis
-    using \<open>((column_size_of M, row_size_of M), map (\<lambda>(v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N))) = ((column_size_of M, row_size_of M), map (\<lambda>(v, w). addV_SP (condenseV v) (condenseV w)) (zip (to_rows M) (to_rows N)))\<close> \<open>condenseM (addM_LIL M N) = ((column_size_of M, row_size_of M), map (\<lambda>(v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N)))\<close> 
+    using \<open>((column_size_of M, row_size_of M), map (\<lambda>(v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N))) = ((column_size_of M, row_size_of M), map (\<lambda>(v, w). addV_SP (condenseV v) (condenseV w)) (zip (to_rows M) (to_rows N)))\<close> \<open>condenseM (addM_LIL M N) = ((column_size_of M, row_size_of M), map (\<lambda>(v, w). condenseV (addV_LIL v w)) (zip (to_rows M) (to_rows N)))\<close>
     by auto
 qed
-    
+
 end
\ No newline at end of file
--- a/Exercises/hwsubm/OR/Madge_Pimentel_Fabio_fabio.madge@tum.de_659/SparseMatrix.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Madge_Pimentel_Fabio_fabio.madge@tum.de_659/SparseMatrix.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,4 +1,12 @@
-(*\<Rightarrow> Simon*)
+(** Score: 6/15
+
+- Definitions for matrices as lists of lists and sparse matrices seem to be good.
+- Definition of multiplication of sparse matrices is missing.
+- Only very basic theorems on regular matrices.
+- No theorems on sparse matrices.
+
+*)
+
 theory SparseMatrix
   imports Complex_Main
 begin
@@ -11,35 +19,35 @@
 
 Ist nicht fertig geworden.
 *)
-  
+
 type_synonym 'a matrix = "'a list list"
 
 find_consts " 'a * 'a   \<Rightarrow> bool"
-  
+
 definition zipWith :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
   "zipWith f xs = map (case_prod f) o zip xs"
-  
+
 definition matrix_add :: "('a::field) matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
   "matrix_add A B \<equiv> zipWith (zipWith (op +)) A B"
-  
+
 definition matrix_mul :: "('a::field) matrix \<Rightarrow> 'a matrix \<Rightarrow> 'a matrix" where
   "matrix_mul A B \<equiv> [[fold op + (zipWith op * a b) 0 . b \<leftarrow> transpose B]. a \<leftarrow> A]"
 
 definition matrix_dim :: "'a matrix \<Rightarrow> nat * nat" where
   "matrix_dim A = (length A, case A of [] \<Rightarrow> 0 | c#_ \<Rightarrow> length c)"
-  
+
 definition matrix_inv :: "'a matrix \<Rightarrow> bool" where
   "matrix_inv A = (\<forall> x \<in> set A. (op = (snd (matrix_dim A)) o length) x)"
-  
+
 value "matrix_add [[1::real,2,3],[4,5,6]] [[3::real,2,1],[4,5,6]]"
-  
+
 lemma matrix_add_preserve_dim: "\<lbrakk>matrix_inv A; matrix_inv B; matrix_dim A = matrix_dim B\<rbrakk> \<Longrightarrow> matrix_dim (matrix_add A B) = matrix_dim A"
   unfolding matrix_add_def zipWith_def matrix_dim_def
   by (simp split: list.splits)
-  
+
 lemma matrix_add_preserve_dim_2: "\<lbrakk>matrix_inv A; matrix_inv B; matrix_dim A = matrix_dim B\<rbrakk> \<Longrightarrow> matrix_dim (matrix_add A B) = matrix_dim B"
   by (simp add: matrix_add_preserve_dim)
-    
+
 
 
 lemma matrix_add_preserve_inv: "\<lbrakk>matrix_inv A; matrix_inv B; matrix_dim A = matrix_dim B\<rbrakk> \<Longrightarrow> matrix_inv (matrix_add A B)"
@@ -49,13 +57,13 @@
 
 lemma swap_swap: "map ((\<lambda>(x, y). y + x) \<circ> prod.swap) (zs::(('a::field * 'a) list)) = map (case_prod op +) zs"
   by auto
-    
+
 lemma comm_vec: "map (case_prod op +) (zip (xs::('a::field list)) ys) = map (case_prod op +) (zip ys xs)"
   by (metis (no_types) swap_swap add.commute case_prod_unfold map_eq_conv map_map prod.swap_def zip_commute)
-    
+
 lemma zipWith_swap: "\<forall>x y. f x y = f y x \<Longrightarrow> map (case_prod f \<circ> prod.swap) (zip xs ys) = map (case_prod f) (zip ys xs)"
   by (metis (no_types, lifting) case_prod_unfold map_eq_conv map_map prod.swap_def zip_commute)
-    
+
 lemma generalize_row:
   assumes "\<forall>x y. f x y = f y x"
   shows "map (\<lambda>(x, y). f x y) (zip xs ys) = map (\<lambda>(x, y). f x y) (zip ys xs)"
@@ -69,10 +77,10 @@
 lemma matrix_add_comm: "matrix_add A B = matrix_add B A"
   unfolding matrix_add_def zipWith_def
   by (auto split: list.splits simp add: add.commute comm_vec generalize_row)
-    
-    
-    
-lemma  "matrix_inv (matrix_mul A B)" 
+
+
+
+lemma  "matrix_inv (matrix_mul A B)"
   unfolding matrix_mul_def matrix_dim_def matrix_inv_def
   by (auto split: list.splits)
 
@@ -83,23 +91,23 @@
   unfolding matrix_mul_def zipWith_def matrix_add_def matrix_dim_def matrix_inv_def
   apply (auto split: list.splits)
   sorry
-    
-lemma 
+
+lemma
   assumes "matrix_inv A" "matrix_inv B" "matrix_inv C" "matrix_dim B = matrix_dim C"
     "snd (matrix_dim A) = fst (matrix_dim B)"
   shows "matrix_mul A (matrix_add B C) = matrix_add (matrix_mul A B) (matrix_mul A C)" using assms
   unfolding matrix_mul_def zipWith_def matrix_add_def matrix_dim_def matrix_inv_def
   apply (auto split: list.splits)
   sorry
-    
+
 
 value "matrix_mul [[1::real,2,3]] [[3,6],[2,4],[4,8]] "
 value "matrix_mul [[1]] (matrix_add [[1::real]] [[2]])"
 value "matrix_mul (matrix_add [[1]] [[1]]) (matrix_add [[1::real]] [[2]])"
 
-  
+
 datatype pos = PS "nat * nat"
- 
+
 instantiation pos :: linorder
 begin
 
@@ -113,6 +121,11 @@
 
 instance
   apply standard
+  (* This is one way you could have done it: *)
+  (*
+  unfolding less_pos_def less_eq_pos_def
+    apply (auto split: pos.splits)
+  *)
   sorry
 
 end
@@ -123,7 +136,7 @@
   "merge _ [] [] = []" |
   "merge _ xs [] = xs" |
   "merge _ [] ys = ys" |
-  "merge f ((p\<^sub>x,x)#xs) ((p\<^sub>y,y)#ys) = (if p\<^sub>x = p\<^sub>y 
+  "merge f ((p\<^sub>x,x)#xs) ((p\<^sub>y,y)#ys) = (if p\<^sub>x = p\<^sub>y
     then (p\<^sub>x, f x y) # (merge f xs ys)
     else (if p\<^sub>x < p\<^sub>y then (p\<^sub>x,x)#(merge f xs ((p\<^sub>y,y)#ys)) else (p\<^sub>y,y)#(merge f ((p\<^sub>x,x)#xs) ys)))"
 
--- a/Exercises/hwsubm/OR/Rdle_Karl_Jonas_jonas.raedle@tum.de_652/Zipper.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Rdle_Karl_Jonas_jonas.raedle@tum.de_652/Zipper.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,3 +1,14 @@
+(** Score: 10/15
+
+  Definition and basic properties of zippers on binary trees. The proofs are all very 
+  simple and some of the proven properties seem a bit superfluous (the "set" ones), as 
+  they are a direct consequence of the "go_*_id" ones. Some important basic properties
+  ("go_up (go_left t) = t"" etc.) are missing.
+
+  One basic correctness properties of Splay Trees was also proven, which is a not so 
+  trivial proof.
+
+*)
 (*\<Rightarrow> Manuel*)
 theory Zipper
 imports
@@ -166,5 +177,4 @@
   apply(rule bst_zipper.cases[of z])
   using bst_zipper_correct by fastforce+
   
-  
 end
\ No newline at end of file
--- a/Exercises/hwsubm/OR/Saporta_Antoine_Jacques_antoine.saporta@tum.de_631/Sparse_Matrix.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Saporta_Antoine_Jacques_antoine.saporta@tum.de_631/Sparse_Matrix.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,6 +1,13 @@
-(*\<Rightarrow> Simon*)
+(** Score: 5/15
+
+- Sparse matrices as sparse vectors of sparse vectors (just as in HOL/Matrix_LP/SparseMatrix.thy)
+- Initial definitions seem to be apt
+- Definition of matrix-vector product seems to be wrong
+- Only very few serious proofs/proof attempts for basic stuff
+
+*)
 theory Sparse_Matrix
-imports Main 
+imports Main
 begin
 
 subsection \<open>Sparse Vector and Matrix Dataype\<close>
@@ -57,10 +64,10 @@
 \<close>
 fun spvec_add_elem :: "('a::monoid_add) spvec \<Rightarrow> 'a  \<Rightarrow> nat \<Rightarrow> 'a spvec" where
   "spvec_add_elem [] x0 i0 = [(x0,i0)]"
-| "spvec_add_elem ((x,i)#xs) x0 i0 = 
-      (if i = i0 then 
+| "spvec_add_elem ((x,i)#xs) x0 i0 =
+      (if i = i0 then
           (if x+x0 = 0 then xs
-           else (x+x0,i)#xs) 
+           else (x+x0,i)#xs)
       else if i < i0 then (x,i)#spvec_add_elem xs x0 i0
       else (x0,i0)#(x,i)#xs)"
 
@@ -71,17 +78,28 @@
 \<close>
 fun add_elem :: "('a::monoid_add) spmat \<Rightarrow> 'a  \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a spmat" where
   "add_elem [] x0 i0 j0 = [([(x0,j0)],i0)]"
-| "add_elem ((v,i)#vs) x0 i0 j0 = 
-      (if i = i0 then 
+| "add_elem ((v,i)#vs) x0 i0 j0 =
+      (if i = i0 then
           (let v1 = spvec_add_elem v x0 j0 in
            if v1=[] then vs
-           else (v1,i)#vs) 
+           else (v1,i)#vs)
       else if i < i0 then (v,i)#add_elem vs x0 i0 j0
       else ([(x0,j0)],i0)#(v,i)#vs)"
 
+(* Added by corrector *)
+lemma spvec_ConsD:
+  "spvec_invar (x # xs) \<Longrightarrow> spvec_invar xs"
+  by (auto simp: spvec_invar_def sorted_Cons)
+
 lemma spvec_add_elem_sorted: "spvec_invar v \<Longrightarrow> sorted (map snd (spvec_add_elem v x0 i0))"
-apply (induction v arbitrary: x0 i0)
-apply (auto simp: spvec_invar_def)
+  apply (induction v arbitrary: x0 i0)
+    (* You could have proceeded like this:
+   apply simp
+  apply (auto dest: spvec_ConsD)
+       apply (frule spvec_ConsD, simp add: sorted_Cons)
+    *)
+    (* Here you can see what kind of argument you were missing *)
+apply (auto simp: spvec_invar_def dest:)
 sorry
 
 lemma spvec_add_elem_distinct: "spvec_invar v \<Longrightarrow> distinct (map snd (spvec_add_elem v x0 i0))"
@@ -100,7 +118,7 @@
 lemma add_elem_spvec_list_invar: "invar m \<Longrightarrow> spvec_list_invar (add_elem m x0 i0 j0)"
 sorry
 
-lemma add_elem_invar[simp]: "invar m \<Longrightarrow> invar (add_elem m x0 i0 j0)" 
+lemma add_elem_invar[simp]: "invar m \<Longrightarrow> invar (add_elem m x0 i0 j0)"
 using add_elem_spvec_invar add_elem_spvec_list_invar invar_def by blast
 
 
@@ -110,7 +128,7 @@
 \<close>
 fun spvec_sum :: "'a::monoid_add spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
   "spvec_sum v1 [] = v1"
-| "spvec_sum v1 ((x,i)#xs) = spvec_sum (spvec_add_elem v1 x i) xs" 
+| "spvec_sum v1 ((x,i)#xs) = spvec_sum (spvec_add_elem v1 x i) xs"
 
 lemma spvec_sum_invar[simp]: "spvec_invar v1 \<Longrightarrow> spvec_invar v2 \<Longrightarrow> spvec_invar (spvec_sum v1 v2)"
 proof (induction v2 arbitrary: v1)
@@ -174,7 +192,7 @@
 
 text \<open>
   Matrix-vector product.
-\<close>  
+\<close>
 definition mat_vec_prod:: "('a::ring) spmat \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
   "mat_vec_prod m v = filter (\<lambda>u. fst u \<noteq> 0) (map (\<lambda>u. (scalar (fst u) v,snd u)) m)"
 
@@ -230,7 +248,7 @@
   Matrix-matrix product.
 \<close>
 definition mat_mat_prod :: "('a::ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
-  "mat_mat_prod m1 m2 =  foldl (\<lambda>m u. sum m (spvec_to_col (fst u) (snd u))) [] (map (\<lambda>u. (mat_vec_prod m1 (fst u),snd u)) (transpose m2))" 
+  "mat_mat_prod m1 m2 =  foldl (\<lambda>m u. sum m (spvec_to_col (fst u) (snd u))) [] (map (\<lambda>u. (mat_vec_prod m1 (fst u),snd u)) (transpose m2))"
 
 lemma mat_mat_prod_invar[simp]: "invar m1 \<Longrightarrow> invar m2 \<Longrightarrow> invar (mat_mat_prod m1 m2)"
 sorry
--- a/Exercises/hwsubm/OR/Stwe_Daniel_daniel.stuewe@tum.de_660/SkewBinHeap.thy	Mon Jul 31 14:54:17 2017 +0200
+++ b/Exercises/hwsubm/OR/Stwe_Daniel_daniel.stuewe@tum.de_660/SkewBinHeap.thy	Wed Aug 02 17:11:04 2017 +0200
@@ -1,7 +1,8 @@
-(** 20/15
+(** 22/15
   Skew binomial heaps and size-height relation.
 
   Missing: get_min, delete_min mset_heap lemma
+    UPDATE: Added 2 hours late by email.
 
 *)
 theory SkewBinHeap
@@ -435,8 +436,40 @@
       qed
     qed
       
+  
+section "Latercomer"  
+      
+(* Too late, but still nice to know *) 
+         
+lemma [simp]: "mset_heap (fold insert ts h) = mset_heap h + mset ts"
+by (induction ts arbitrary: h) auto
+  
+lemma [simp]: "(\<forall> t \<in> set h. bin_skew_invar t) \<Longrightarrow> image_mset tree.root (mset [t\<leftarrow>h . rank t = 0]) = mset_heap [t\<leftarrow>h . rank t = 0]"
+by (induction h) auto 
     
-(* I got some type errors when I wanted to show the bootstraping as in the paper that's why 
+lemma aux2: "(\<forall> t \<in> set h. bin_skew_invar t) \<Longrightarrow>
+     mset_heap [t\<leftarrow>h . 0 < rank t] + image_mset tree.root (mset [t\<leftarrow>h . rank t = 0]) = mset_heap h" 
+by (induction h) auto 
+    
+lemma getMin_mset_heap[simp]:    
+  assumes "getMin ts = (t',ts')" and  "ts\<noteq>[]"
+  shows "mset_heap ts = mset_tree t' + mset_heap ts'"
+  using assms
+  by (induction ts arbitrary: t' ts' rule: find_min.induct)
+     (auto split: prod.splits if_splits)  
+     
+lemma invar_children[simp]: "bin_skew_invar t \<Longrightarrow> x \<in> set (children t) \<Longrightarrow> bin_skew_invar x"
+  by (induction t arbitrary: x rule: bin_skew_invar.induct) (auto simp: bin_skew_invar.intros(1))  
+    
+theorem "bin_skew_heap_invar h \<Longrightarrow> h \<noteq> [] \<Longrightarrow> mset_heap (deleteMin h) =  mset_heap h - {# findMin h #}" 
+  apply (auto simp add: algebra_simps split: tree.splits prod.splits)
+  apply (subst aux2)
+  by (auto dest: getMin_findMin_same_root getMin_heap_invar)
+    
+ 
+section "Bootstrapping"    
+    
+(* I got some type errors when I wanted to show the bootstrapping as in the paper that's why 
    it's not included *)
     
 end
\ No newline at end of file