diff -r 38cde0214ad5 -r c33cfa1e813a thys/notes.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/notes.tex	Thu Jan 29 23:39:08 2015 +0000
@@ -0,0 +1,121 @@
+\documentclass[11pt]{article}
+
+\begin{document}
+
+\noindent
+A lemma which might be true, but can also be false, is as follows:
+
+\begin{center}
+\begin{tabular}{lll}
+If   & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\
+     & (2) & $\vdash v_1 : der\;c\;r$, and\\ 
+     & (3) & $\vdash v_2 : der\;c\;r$ holds,\\
+then &     & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds.  
+\end{tabular}
+\end{center}
+
+\noindent It essentially states that if one value $v_1$ is 
+bigger than $v_2$ then this ordering is preserved under 
+injections. This is proved by induction (on the definition of 
+$der$\ldots this is very similar to an induction on $r$).
+\bigskip
+
+\noindent
+The case that is still unproved is the sequence case where we 
+assume $r = r_1\cdot r_2$ and also $r_1$ being nullable.
+The derivative $der\;c\;r$ is then
+
+\begin{center}
+$der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$
+\end{center}
+
+\noindent 
+or without the parentheses
+
+\begin{center}
+$der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$
+\end{center}
+
+\noindent 
+In this case the assumptions are
+
+\begin{center}
+\begin{tabular}{ll}
+(a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\
+(b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
+(c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\
+(d) & $nullable(r_1)$
+\end{tabular}
+\end{center}
+
+\noindent 
+The induction hypotheses are
+
+\begin{center}
+\begin{tabular}{ll}
+(IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2
+\;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\; 
+\vdash v_2 : der\;c\;r_1\qquad$\\
+      & $\hfill\longrightarrow
+         inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\
+(IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2
+\;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\; 
+\vdash v_2 : der\;c\;r_2\qquad$\\
+      & $\hfill\longrightarrow
+         inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\
+\end{tabular}
+\end{center}
+
+\noindent 
+The goal is
+
+\[
+(goal)\qquad
+inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2} 
+inj\; (r_1 \cdot r_2)\;c\;v_2
+\]
+
+\noindent 
+If we analyse how (a) could have arisen (that is make a case
+distinction), then we will find four cases:
+
+\begin{center}
+\begin{tabular}{ll}
+LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\
+LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\
+RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\
+RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\
+\end{tabular}
+\end{center}
+
+
+\noindent 
+We have to establish our goal in all four cases. 
+
+
+\subsubsection*{Case LR}
+
+The corresponding rule (instantiated) is:
+
+\begin{center}
+\begin{tabular}{c}
+$len\,|w_1| \geq len\,|w_2|$\\
+\hline
+$Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$
+\end{tabular}
+\end{center}
+
+\subsubsection*{Case RL}
+
+The corresponding rule (instantiated) is:
+
+\begin{center}
+\begin{tabular}{c}
+$len\,|w_1| > len\,|w_2|$\\
+\hline
+$Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$
+\end{tabular}
+\end{center}
+
+
+\end{document}