diff -r db0ff630bbb7 -r 43e070803c1c thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Thu Apr 11 17:37:00 2019 +0100
+++ b/thys/Journal/Paper.thy	Fri May 10 11:56:37 2019 +0100
@@ -1686,6 +1686,73 @@
 *}
 
 
+section {* HERE *}
+
+text {*
+  \begin{center}
+  \begin{tabular}{llcl}
+  1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\
+  2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\
+  3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\
+  4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\
+  4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\
+  4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ & 
+        @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\
+  5) & @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\
+  6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\
+  \end{tabular}
+  \end{center}
+
+  \begin{lemma}
+  @{thm [mode=IfThen] bder_retrieve}
+  \end{lemma}
+
+  \begin{proof}
+  By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are
+  straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to 
+  @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)
+  where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption
+  we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by 
+  simplification of left- and right-hand side. In  case @{term "c \<noteq> d"} we have again
+  @{term "\<Turnstile> v : ZERO"}, which cannot  hold. 
+
+  For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b).
+  The  induction hypothesis is 
+  \[
+  @{term "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"}
+  \]
+  which is what left- and right-hand side simplify to.  The slightly more interesting case
+  is for 4c). By assumption  we have 
+  @{term "\<Turnstile> v : ALT (der c (erase r\<^sub>1)) (der c (erase (AALTs bs (r\<^sub>2 # rs))))"}. This means we 
+  have either (*) @{term "\<Turnstile> v1 : der c (erase r\<^sub>1)"} with @{term "v = Left v1"} or
+  (**) @{term "\<Turnstile> v2 : der c (erase (AALTs bs (r\<^sub>2 # rs)))"} with @{term "v = Right v2"}.
+  The former  case is straightforward by simplification. The second case is \ldots TBD.
+
+  Rule 5) TBD.
+
+  Finally for rule 6) the reasoning is as follows:   By assumption we  have
+  @{term "\<Turnstile> v : SEQ (der c (erase r)) (STAR (erase r))"}. This means we also have
+  @{term "v = Seq v1 v2"}, @{term "\<Turnstile> v1 : der c (erase r)"}  and @{term "v2 = Stars vs"}.
+  We want to prove
+  \begin{align}
+  & @{term "retrieve (ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)) v"}\\
+  &= @{term "retrieve (ASTAR bs r) (injval (STAR (erase r)) c v)"}
+  \end{align}
+  The right-hand side @{term inj}-expression is equal to 
+  @{term "Stars (injval (erase r) c v1 # vs)"}, which means the @{term  retrieve}-expression
+  simplifies to 
+  \[
+  @{term "bs @ [Z] @ retrieve r (injval (erase r) c v1) @ retrieve (ASTAR [] r) (Stars vs)"}
+  \]
+  The left-hand side (3) above simplifies to 
+  \[
+  @{term "bs @ retrieve (fuse [Z] (bder c r)) v1 @ retrieve (ASTAR [] r) (Stars vs)"} 
+  \]
+  We can move out the @{term "fuse  [Z]"} and then use the IH to show that left-hand side
+  and right-hand side are equal. This completes the proof. 
+  \end{proof}   
+*}
+
 
 
 (*<*)