# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1422574748 0
# Node ID c33cfa1e813adf8997b3209b93b9251ac39e0a2a
# Parent  38cde0214ad52359e189c4bd277736f9111a78db
added some notes (still incomplete)

diff -r 38cde0214ad5 -r c33cfa1e813a thys/Re1.thy
--- a/thys/Re1.thy	Thu Jan 29 09:05:40 2015 +0000
+++ b/thys/Re1.thy	Thu Jan 29 23:39:08 2015 +0000
@@ -724,192 +724,19 @@
 lemma t: "(c#xs = c#ys) \<Longrightarrow> xs = ys"
 by (metis list.sel(3))
 
-lemma Prf_proj:
-  assumes "v1 \<succ>r v2" "\<turnstile> v1 : r" "\<turnstile> v2 : r" "\<exists>s. (flat v1) = c # s" "\<exists>s. (flat v2) = c # s"
-  shows "(projval r c v1) \<succ>(der c r) (projval r c v2)"
-using assms
-apply(induct arbitrary: v1 v2 rule: der.induct)
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(case_tac "c = c'")
-apply(simp)
-apply (metis ValOrd.intros(7))
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(simp)
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(simp)
-apply(auto)
-defer
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply (metis Prf_flat_L nullable_correctness)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros(2))
-apply (metis append_Cons list.inject neq_Nil_conv)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(auto)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(auto)[1]
-apply(rule ValOrd.intros)
-apply metis
-apply(clarify)
-apply(rule ValOrd.intros)
-
-apply(rule ValOrd.intros)
-apply(simp)
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(rule ValOrd.intros)
-defer
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp add: append_eq_Cons_conv)
-apply(clarify)
-apply(rule ValOrd.intros)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-apply(subst v4_proj2)
-apply(simp)
-apply(simp)
-
-apply(simp)
-
-apply (metis Prf_flat_L nullable_correctness)
-
-
-
-
-apply(rule ValOrd.intros(2))
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(simp)
-apply(erule ValOrd.cases)
-apply(simp_all)[8]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(erule Prf.cases)
-apply(simp_all)[5]
-apply(clarify)
-apply(simp)
-
 lemma Prf_inj:
   assumes "v1 \<succ>(der c r) v2" "\<turnstile> v1 : der c r" "\<turnstile> v2 : der c r"
   shows "(injval r c v1) \<succ>r (injval r c v2)"
 using assms
 apply(induct arbitrary: v1 v2 rule: der.induct)
+(* NULL case *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* EMPTY case *)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* CHAR case *)
 apply(case_tac "c = c'")
 apply(simp)
 apply(erule ValOrd.cases)
@@ -918,6 +745,7 @@
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
+(* ALT case *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
@@ -956,6 +784,7 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* SEQ case*)
 apply(simp)
 apply(case_tac "nullable r1")
 defer
@@ -976,10 +805,12 @@
 apply(simp_all)[5]
 apply(erule Prf.cases)
 apply(simp_all)[5]
+(* nullable case - unfinished *)
 apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 apply(clarify)
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(erule Prf.cases)
@@ -994,10 +825,8 @@
 apply(simp)
 apply (metis impossible_Cons le_add2 list.size(3) mkeps_flat monoid_add_class.add.right_neutral v4)
 apply(rule ValOrd.intros(2))
-
-apply(rotate_tac 1)
-apply(drule meta_mp)
-apply(rule
+apply(drule_tac x="proj r1 c" in spec)
+oops
 
 lemma POSIX_der:
   assumes "POSIX v (der c r)" "\<turnstile> v : der c r"
@@ -1005,10 +834,10 @@
 using assms
 unfolding POSIX_def
 apply(auto)
+thm v4
 apply(subst (asm) v4)
 apply(assumption)
 apply(drule_tac x="projval r c v'" in spec)
-apply(drule mp)
 apply(auto)
 apply(rule v3_proj)
 apply(simp)
diff -r 38cde0214ad5 -r c33cfa1e813a thys/notes.pdf
Binary file thys/notes.pdf has changed
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}