1689 section {* HERE *}

  1690 

  1691 text {*

  1692   \begin{center}

  1693   \begin{tabular}{llcl}

  1694   1) & @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\

  1695   2) & @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\

  1696   3) & @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\

  1697   4a) & @{term "erase (AALTs bs [])"} & $\dn$ & @{term ZERO}\\

  1698   4b) & @{term "erase (AALTs bs [r])"} & $\dn$ & @{term "erase r"}\\

  1699   4c) & @{term "erase (AALTs bs (r\<^sub>1#r\<^sub>2#rs))"} & $\dn$ & 

  1700         @{term "ALT (erase r\<^sub>1) (erase (AALTs bs (r\<^sub>2#rs)))"}\\

  1701   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"]}\\

  1702   6) & @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\

  1703   \end{tabular}

  1704   \end{center}

  1705 

  1706   \begin{lemma}

  1707   @{thm [mode=IfThen] bder_retrieve}

  1708   \end{lemma}

  1709 

  1710   \begin{proof}

  1711   By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are

  1712   straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to 

  1713   @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3)

  1714   where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption

  1715   we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by 

  1716   simplification of left- and right-hand side. In  case @{term "c \<noteq> d"} we have again

  1717   @{term "\<Turnstile> v : ZERO"}, which cannot  hold. 

  1718 

  1719   For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b).

  1720   The  induction hypothesis is 

  1721   \[

  1722   @{term "retrieve (bder c r) v = retrieve r (injval (erase r) c v)"}

  1723   \]

  1724   which is what left- and right-hand side simplify to.  The slightly more interesting case

  1725   is for 4c). By assumption  we have 

  1726   @{term "\<Turnstile> v : ALT (der c (erase r\<^sub>1)) (der c (erase (AALTs bs (r\<^sub>2 # rs))))"}. This means we 

  1727   have either (*) @{term "\<Turnstile> v1 : der c (erase r\<^sub>1)"} with @{term "v = Left v1"} or

  1728   (**) @{term "\<Turnstile> v2 : der c (erase (AALTs bs (r\<^sub>2 # rs)))"} with @{term "v = Right v2"}.

  1729   The former  case is straightforward by simplification. The second case is \ldots TBD.

  1730 

  1731   Rule 5) TBD.

  1732 

  1733   Finally for rule 6) the reasoning is as follows:   By assumption we  have

  1734   @{term "\<Turnstile> v : SEQ (der c (erase r)) (STAR (erase r))"}. This means we also have

  1735   @{term "v = Seq v1 v2"}, @{term "\<Turnstile> v1 : der c (erase r)"}  and @{term "v2 = Stars vs"}.

  1736   We want to prove

  1737   \begin{align}

  1738   & @{term "retrieve (ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)) v"}\\

  1739   &= @{term "retrieve (ASTAR bs r) (injval (STAR (erase r)) c v)"}

  1740   \end{align}

  1741   The right-hand side @{term inj}-expression is equal to 

  1742   @{term "Stars (injval (erase r) c v1 # vs)"}, which means the @{term  retrieve}-expression

  1743   simplifies to 

  1744   \[

  1745   @{term "bs @ [Z] @ retrieve r (injval (erase r) c v1) @ retrieve (ASTAR [] r) (Stars vs)"}

  1746   \]

  1747   The left-hand side (3) above simplifies to 

  1748   \[

  1749   @{term "bs @ retrieve (fuse [Z] (bder c r)) v1 @ retrieve (ASTAR [] r) (Stars vs)"} 

  1750   \]

  1751   We can move out the @{term "fuse  [Z]"} and then use the IH to show that left-hand side

  1752   and right-hand side are equal. This completes the proof. 

  1753   \end{proof}   

  1754 *}

  1755