(*ML {* add_path "~~/src/HOL/Matrix";*}*)

(*<*)
theory blatt8 = Matrix:
(*>*)

section {* Matrizen *}

text {*
Matrizen sind bekannt aus der Linearen Algebra. Im abschließenden Projekt werden wir 
\begin{itemize}
\item
  eine Darstellung schwach besetzter Matrizen definieren,
\item
  für diese Darstellung Operationen wie Multiplikation definieren,
\item
  und diese Operationen unter gewissen Voraussetzungen als korrekt beweisen.
\end{itemize}

Wir werden hierzu nicht wie sonst auf der Isabelle-Theorie \texttt{Main}, sondern auf der Theorie \texttt{Matrix} aufbauen, die grundlegende 
Definitionen und Sätze für Matrizen zur Verfügung stellt. Um diese Theorie in ProofGeneral benutzen zu können, fügen Sie am Anfang Ihrer Theorie folgende Zeile hinzu:
\begin{center}
\loadMyHOLMatrix
\end{center}
Dies erlaubt es dem System, die Theorien \texttt{Matrix} und \texttt{MatrixGeneral} zu finden. Weiterhin müssen Sie, um diese Theorien verwenden zu 
können, die neueste Version von Isabelle ausführen:
\begin{center}
  \texttt{/usr/proj/isabelle/IsabelleCurrent/bin/Isabelle}
\end{center}

Matrizen sind (in \texttt{MatrixGeneral}) als polymorpher Typ
@{typ "'a matrix"} definiert. Eine Instanz dieses polymorphen Typs ist beispielsweise @{typ "int matrix"}, der Typ derjenigen Matrizen, deren Elemente
ganze Zahlen sind. Typvariablen wie @{typ "'a"} können eingeschränkt werden durch Angabe einer \emph{Typklasse}.
Informieren Sie sich in Abschnitt 8.4 von \emph{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic} über axiomatische Typklassen. 
Im folgenden werden wir uns nur mit Matrizen vom Typ @{typ [show_sorts] "('a::lordered_ring) matrix"} beschäftigen, d.h. mit Matrizen, deren Elemente u.a. einen partiell geordneten Ring formen.

Matrizen in Isabelle sind nach folgender Vorstellung gebildet: Eine Matrix ist ein zwei-dimensionales unendliches Array, so dass nur endlich viele 
Elemente dieses Arrays von $0$ verschieden sind. Gegeben eine Matrix $A$, so kann auf das Element $A_{ji}$ in der $j$-ten Zeile und $i$-ten Spalte über
@{term "Rep_matrix A j i"} zugegriffen werden. Die Anzahl der Zeilen von $A$ wird durch @{term "nrows A"} bezeichnet, die Anzahl der Spalten durch 
@{term "ncols A"} (überlegen Sie sich, was Anzahl der Zeilen/Spalten in obiger Vorstellung von Matrizen bedeutet).

Weiterhin sind Addition, Multiplikation mit einem Skalar, und Multiplikation zweier Matrizen $A$ und $B$ für alle Zeilen $j$ und Spalten $i$ 
definiert durch (die exakten Definitionen finden Sie in \texttt{Matrix} und \texttt{MatrixGeneral})
\begin{mymath}
(A+B)_{ji} = A_{ji}+ B_{ji}, \quad (\operatorname{scalar\_mult}\ c\ A)_{ji} = c * A_{ji}, \quad (A*B)_{ji} = \sum_{k} A_{jk} * B_{ki}.    
\end{mymath}

Schließlich können diese zwei Funktionen zur Erstellung neuer Matrizen und zur strukturellen Modifikation von Matrizen verwendet werden:
\begin{itemize}
\item @{term "singleton_matrix j i x"} repräsentiert diejenige Matrix $A$ mit @{term "Rep_matrix A j i = x"} und @{text "Rep_matrix A u v = 0"} für
$u \neq j$ oder $v \neq i$,
\item @{term "move_matrix A j i"} repräsentiert diejenige Matrix $B$, die aus $A$ durch Verschiebung von $j$ Zeilen nach unten und $i$ Spalten nach 
rechts entsteht.
\end{itemize}
*}

(*<*)
consts
  mE1 :: "int matrix"
  mE2 :: "int matrix"
  mA :: "int matrix"
  mB :: "int matrix"

lemma mE1_E2: "mE1 = move_matrix mE2 (-1) (-1)" 
  sorry 

lemma ncols_A: "ncols mA = 2" 
  sorry

lemma nrows_B: "nrows mB = 2"
  sorry

lemma mult_A_B: "mE2 = mA * mB"
  sorry
(*>*)

text {* 
\textbf{Aufgabe 1}: Definieren Sie konstante Matrizen $mE1$, $mE2$, $mA$, $mB$ vom Typ @{typ "int matrix"} mit den Werten
\begin{mymath}
  mE1 = \begin{pmatrix} 1 \end{pmatrix}, \quad
  mE2 = \begin{pmatrix} 1 & 0 \\ 0 & 1 \end{pmatrix}, \quad
  mA = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}, \quad
  mB = \begin{pmatrix} 1 & -1 \\ 0 & 1 \end{pmatrix}.
\end{mymath}   
Benutzen Sie dabei für die Definition von $mE1$ und $mE2$ nicht die Funktion @{term "move_matrix"}, und für die Definition von $mA$ und $mB$ verzichten
Sie bitte auf die Verwendung von @{term "singleton_matrix"} (Sie dürfen aber auf $mE1$ und $mE2$ zurückgreifen). Zeigen Sie:
\begin{enumerate}
\item @{thm mE1_E2},
\item @{thm ncols_A}, 
\item @{thm nrows_B},
\item @{thm mult_A_B}.
\end{enumerate} 
Tip: Machen Sie Gebrauch von Lemmata aus \texttt{MatrixGeneral}:
 @{text "Rep_matrix_inject"}, @{text "ncols_le"}, @{text "le_ncols"}, @{text "nrows_le"}, @{text "le_nrows"},
 @{text "Rep_matrix_mult"}. Im Zusammenhang mit Integer-Arithmetik vergessen Sie nicht die @{text arith}-Methode und die Lemmata
  @{text "numerals"}, @{text "neg_def"}.  
*}

section {* Schwach besetzte Matrizen *}

text{* Das Rechnen mit Matrizen, die über Funktionen wie @{term "singleton_matrix"} oder @{term "move_matrix"} definiert wurden, ist, wie wir 
gesehen haben, möglich, aber umständlich. Es wäre schön, das Rechnen mit Matrizen zu systematisieren. Hierzu müssen wir Matrizen auf geeignetere 
Weise repräsentieren. Prinzipiell gibt es zwei Möglichkeiten, eine Matrix konkret aufzuschreiben:
\begin{enumerate}
\item Man wählt eine \emph{dichte} Darstellung, und listet alle Elemente der Matrix nach Zeilen und Spalten geordnet auf, beispielsweise:
\begin{mymath}
\begin{pmatrix} 0 & 4 & 0 \\ 3 & 0 & 7 \\ 0 & 0 & 0 \\ 8 & 0 & 0 \end{pmatrix}.
\end{mymath}
\item Man wählt eine Darstellung, die gut für \emph{schwach besetzte} Matrizen geeignet ist. Hier verzichtet man darauf, alle Elemente der Matrix 
aufzuschreiben, indem man die Position der Elemente innerhalb der Matrix beachtet und versucht, Redundanzen auszunutzen. 
\end{enumerate}
Wir wählen die zweite Darstellungsweise. Eine einfache Möglichkeit, um schwach besetzte Matrizen zu repräsentieren, ist die Darstellung als Liste von 
Listen, wobei die Elemente der Listen jeweils mit einem Index versehen sind, der die Position des Elements innerhalb der Matrix beschreibt.
*}

types 
  'a spvec = "(nat * 'a) list"
  'a spmat = "('a spvec) spvec"

(*<*)
constdefs
  spmat_A :: "int spmat"
  "spmat_A == [(0, [(1, 4)]), (1, [(0, 3), (2, 7)]), (3, [(0,8)])]"
  spmat_B :: "int spmat"
  "spmat_B == [(0, [(1, 4)]), (1, [(2, 7), (0, 3)]), (3, [(0,8)])]"
  spmat_C :: "int spmat"
  "spmat_C == [(0, [(0, 0), (1, 4), (2,0), (3,0)]), (1, [(0, 3), (2, 3), (1, 0), (2, 4)]), (3, [(0,2),(2,-1)]), (3, [(2, 1),(0,6)])]"
(*>*)

text {* 
Obige Matrix könnte dabei wie folgt als @{typ "int spmat"} dargestellt werden:
\begin{center}
@{thm spmat_A_def}. 
\end{center}
Dies ist auch eine zulässige Darstellung derselben Matrix:
\begin{center}
@{thm spmat_B_def}.
\end{center}
Und hier noch eine dritte Möglichkeit:
\begin{center}
  @{thm spmat_C_def}.
\end{center}

\noindent\textbf{Aufgabe 2}: Definieren Sie durch primitive Rekursion Funktionen, die Argumente vom Typ @{typ "'a spvec"} bzw. @{typ "'a spmat"} 
als Matrizen interpretieren:
*}   
consts
  sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix"
  sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix"

text {* Benutzen Sie bei der Definition von
@{term "sparse_row_vector"} die Funktion @{term "singleton_matrix"}, und bei der Definition von @{term "sparse_row_matrix"}
die Funktion @{term "move_matrix"}. *}

(*<*)

lemma sparse_row_vector_append[simp]: "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
  sorry

lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
  sorry

lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)"
  sorry

lemma spmat_A_eq_spmat_B: "sparse_row_matrix spmat_A = sparse_row_matrix spmat_B"
  sorry

lemma spmat_A_eq_spmat_C: "sparse_row_matrix spmat_A = sparse_row_matrix spmat_C"
  sorry
(*>*)

text {* 
Fügen Sie Ihrem Repertoire an Lemmata  @{text "ring_eq_simps"} und @{text "add_nrows"} hinzu. Zeigen Sie nun:
\begin{enumerate} 
\item @{thm spmat_A_eq_spmat_B}
\item @{thm spmat_A_eq_spmat_C}
\item @{thm [display,margin=70] nrows_spvec [no_vars]}
\item @{thm [display,margin=70] sparse_row_vector_append [no_vars]}
\item @{thm [display,margin=70] sparse_row_matrix_append [no_vars]}
\end{enumerate}
*}

section {* Sortierung *}

text {*
Zwei Sortierungsbegriffe werden sich als nützlich erweisen:
*}

consts
  sorted_spvec :: "'a spvec \<Rightarrow> bool"
  sorted_spmat :: "'a spmat \<Rightarrow> bool"

primrec
  "sorted_spmat [] = True"
  "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"

(*<*)

lemma sorted_sparse_row_vector_zero[rule_format]: "m <= n \<longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_vector arr) j m = 0"
  sorry

lemma sorted_sparse_row_matrix_zero[rule_format]: "m <= n \<longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_matrix arr) m j = 0"
  sorry

lemma sorted_spmat_A: "(sorted_spvec spmat_A) & (sorted_spmat spmat_A)"
  sorry

lemma sorted_spmat_B: "(sorted_spvec spmat_B) & ~(sorted_spmat spmat_B)"
  sorry

lemma sorted_spmat_C: "~ (sorted_spvec spmat_C | sorted_spmat spmat_C)"
  sorry
(*>*)

text {* 
\noindent\textbf{Aufgabe 3}: Definieren Sie @{term sorted_spvec} durch primitive Rekursion und zeigen Sie folgende Eigenschaften: 
\begin{enumerate}
\item @{thm "sorted_spmat_A"}
\item @{thm "sorted_spmat_B"}
\item @{thm "sorted_spmat_C"}
\item @{thm [display,margin=70] sorted_sparse_row_vector_zero [no_vars]}
\item @{thm [display,margin=70] sorted_sparse_row_matrix_zero [no_vars]}
\end{enumerate}
*}

section {* Multiplikation schwach besetzter Matrizen *}

text {*
Wie schon im ersten Teil erwähnt, lässt sich das Produkt $C$ zweier Matrizen $A$ und $B$ definieren durch
\begin{mymath}
  C_{ji} = \sum_k A_{jk} B_{ki}.
\end{mymath}
Nun ist diese Berechnungsweise nicht besonders gut geeignet, wenn wir einen Vorteil daraus ziehen möchten, dass wir es mit schwach 
besetzten Matrizen zu tun haben. Lassen wir in obiger Formel bei $C$ und $B$ die Spaltenindizes weg, so erhalten wir
\begin{mymath}
  C_j = \sum_k A_{jk} B_k.
\end{mymath}
Man erhält also die $j$-te Zeile von $C$, indem man die Zeilen von $B$, mit den entsprechenden Konstanten aus der $j$-ten Zeile von $A$ multipliziert,
aufaddiert. 

\noindent\textbf{Aufgabe 4}: Definieren Sie eine Funktion @{text addmult_spvec}, die zum Aufaddieren der gewichteten Zeilen von $B$ benutzt werden kann:
*}

consts
  addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"

(*<*)

lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) = (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
  sorry

lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
  sorry


lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec (y, a, b))"
  sorry
(*>*)

text {*
Diese Funktion soll ihre beiden Argumentlisten nur einmal durchlaufen, und die nachfolgenden Eigenschaften erfüllen.
Beweisen Sie die erste dieser Eigenschaften:
\begin{enumerate}
\item @{thm [display,margin=70] "sparse_row_vector_addmult_spvec" [no_vars]}
\item @{thm [display,margin=70] "sorted_addmult_spvec" [no_vars]}
\end{enumerate}
*}

text {*
Mithilfe von @{term addmult_spvec} sind wir nun in der Lage, eine Zeile des Produktes zweier Matrizen auf die 
weiter oben beschriebene Weise zu berechnen:
*}  

consts 
  mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat  \<Rightarrow> 'a spvec"

(*<*)
lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> 
  sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
  sorry

lemma sorted_mult_spvec_spmat[rule_format]: 
  "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))"
  sorry

(*>*)

text {*
\noindent\textbf{Aufgabe 5}: Definieren Sie @{term mult_spvec}. Auch hier sollen die Argumentlisten nur einmal durchlaufen werden. 
Die zu erfüllenden Eigenschaften lauten:  
\begin{enumerate}
\item @{thm [display,margin=70] sparse_row_mult_spvec_spmat [no_vars]}
\item @{thm [display,margin=70] sorted_mult_spvec_spmat [no_vars]}
\end{enumerate}
Zeigen Sie Eigenschaft Nr. 1.

\noindent\textbf{Aufgabe 6}: Definieren Sie eine Funktion zur Berechnung des Produktes zweier  
Matrizen in (ggf. sortierter) @{text spmat}-Darstellung und zeigen Sie ihre Korrektheit. 
*}

(*<*)  
consts 
  mult_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"

lemma sparse_row_mult_spmat[rule_format]: 
  "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
  sorry


end
(*>*)