--- a/thys/Re1.thy	Thu Feb 26 12:51:02 2015 +0000
+++ b/thys/Re1.thy	Thu Feb 26 16:35:10 2015 +0000
@@ -345,22 +345,30 @@
 apply (rule ValOrd.intros(2))
 apply metis
 apply(simp)
+(* ALT case *)
 apply(simp)
 apply(erule disjE)
 apply(simp)
 apply (metis POSIX_ALT_I1)
-apply(auto)
+(* *)
+apply(auto)[1]
+thm  POSIX_ALT_I1
 apply (metis POSIX_ALT_I1)
-apply(simp add: POSIX_def)
+apply(simp (no_asm) add: POSIX_def)
 apply(auto)[1]
-apply (metis Prf.intros(3))
-apply(rotate_tac 5)
+apply(rule Prf.intros(3))
+apply(simp only: POSIX_def)
+apply(rotate_tac 4)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(simp add: mkeps_flat)
 apply(auto)[1]
+thm Prf_flat_L nullable_correctness
 apply (metis Prf_flat_L nullable_correctness)
 apply(rule ValOrd.intros)
+apply(subst (asm) POSIX_def)
+apply(clarify)
+apply(drule_tac x="v2" in spec)
 by metis
 
 
@@ -401,8 +409,8 @@
 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
   "projval (CHAR d) c _ = Void"
-| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
-| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)"
+| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
+| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
      (if flat v1 = [] then Right(projval r2 c v2) 
       else if nullable r1 then Left (Seq (projval r1 c v1) v2)

Binary file thys/notes.pdf has changed

--- a/thys/notes.tex	Thu Feb 26 12:51:02 2015 +0000
+++ b/thys/notes.tex	Thu Feb 26 16:35:10 2015 +0000
@@ -3,7 +3,7 @@
 \usepackage{amsmath}
 
 \begin{document}
-%%\linenumbers
+%%%\linenumbers
 
 \noindent 
 We already proved that
@@ -348,6 +348,33 @@
 \end{tabular}
 \end{center}
 
+\subsection*{Test Proof}
+
+We want to prove that
+
+\[
+nullable(r) \;\text{implies}\; POSIX (mkeps\; r)\; r
+\]
+
+\noindent
+We prove this by induction on $r$. There are 5 subcases, and 
+only the $r_1 + r_2$-case is interesting. In this case we know the 
+induction hypotheses are
+
+\begin{center}
+\begin{tabular}{ll}
+(IMP1) & $nullable(r_1) \;\text{implies}\; 
+          POSIX (mkeps\; r_1)\; r_1$ \\
+(IMP2) & $nullable(r_2) \;\text{implies}\;
+          POSIX (mkeps\; r_2)\; r_2$
+\end{tabular}
+\end{center}
+
+\noindent and know that $nullable(r_1 + r_2)$ holds. From this
+we know that either $nullable(r_1)$ holds or $nullable(r_2)$.
+Let us consider the first case where we know $nullable(r_1)$.
+
+
 \subsection*{Problems in the paper proof}
 
 I cannot verify