author lammich Wed, 02 Aug 2017 17:11:04 +0200 changeset 69886 4abb5f2c0363 parent 69883 01e3de0b7352 child 69887 3880061ed9fb
more bonus corr
```--- 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.
-
+

-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"
-
-definition addM_LIL :: "matrix_LIL \<Rightarrow> matrix_LIL \<Rightarrow> matrix_LIL" where
+value "retrieveM_LIL (zeroM_LIL 100 200) 200 3"
+
+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)
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"
-
+
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
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
@@ -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)"

-
-definition addM_SP :: "matrix_SP \<Rightarrow> matrix_SP \<Rightarrow> matrix_SP" where
+
+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
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 @@
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)))"
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)))"
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
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))"
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))"
@@ -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"
-
+
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)))"
@@ -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))"
hence "set (to_list_SP v') = Set.filter (\<lambda> (i, x). x \<noteq> 0) (set (zip [0..<k] l))"
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)))"
-  also have "\<dots> = length (map condenseV (to_rows M))"
+  also have "\<dots> = length (map condenseV (to_rows M))"
also have "\<dots> = length (to_rows M)"
by simp
thus ?thesis
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))]"
-    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"
-  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"

@@ -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)))"
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
oops
-
+
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
qed
-
+
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

-
-
-
+
+
+

@@ -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
-
+
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))))"
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
-
+
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
-
+
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
-
+
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)"
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."
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)))"
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)"
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
@@ -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)"
-
+
-
+
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"
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"
-
+

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_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]])"

-
+
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)"

+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 @@
sorry

@@ -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```