(*<*)
theory Slides2
imports "../thys/UTM" "../thys/Abacus_Defs"
begin
declare [[show_question_marks = false]]

hide_const (open) s 

abbreviation
  "update2 p a \<equiv> update a p"

notation (Rule output)
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("_")

context uncomputable
begin

notation (latex output)
  Cons ("_::_" [48,47] 68) and
  append ("_@_" [65, 64] 65) and
  Oc ("1") and
  Bk ("0") and
  exponent ("_\<^bsup>_\<^esup>" [107] 109) and
  inv_begin0 ("I\<^sub>0") and
  inv_begin1 ("I\<^sub>1") and
  inv_begin2 ("I\<^sub>2") and
  inv_begin3 ("I\<^sub>3") and
  inv_begin4 ("I\<^sub>4") and 
  inv_begin ("I\<^bsub>cbegin\<^esub>") and
  inv_loop1 ("J\<^sub>1") and
  inv_loop0 ("J\<^sub>0") and
  inv_end1 ("K\<^sub>1") and
  inv_end0 ("K\<^sub>0") and
  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
  Pr ("Pr\<^sup>_") and
  Cn ("Cn\<^sup>_") and
  Mn ("Mn\<^sup>_") and
  tcopy ("copy") and 
  tcontra ("contra") and
  tape_of ("\<langle>_\<rangle>") and 
  code_tcontra ("code contra") and
  tm_comp ("_ ; _") 

 
lemma inv_begin_print:
  shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
        "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
        "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 
        "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 
        "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and
        "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"
apply(case_tac [!] tp)
by (auto)


lemma inv1: 
  shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
unfolding Turing_Hoare.assert_imp_def
unfolding inv_loop1.simps inv_begin0.simps
apply(auto)
apply(rule_tac x="1" in exI)
apply(auto simp add: replicate.simps)
done

lemma inv2: 
  shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
apply(rule ext)
apply(case_tac x)
apply(simp add: inv_end1.simps)
done


lemma measure_begin_print:
  shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
        "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
        "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
        "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
by (simp_all)

lemma inv_begin01:
  assumes "n > 1"
  shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"
using assms by auto                          

lemma inv_begin02:
  assumes "n = 1"
  shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
using assms by auto

(*>*)



text_raw {*
  \renewcommand{\slidecaption}{ITP, 24 July 2013}
  \newcommand{\bl}[1]{#1}                        
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\[-3mm]
  {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 
  {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 
  \end{tabular}}
  
  \bigskip\medskip\medskip
 
  \begin{center}
  \begin{tabular}{c@ {\hspace{1cm}}c}
  \includegraphics[scale=0.29]{jian.jpg}  &
  \includegraphics[scale=0.034]{xingyuan.jpg} \\
  Jian Xu & Xingyuan Zhang\\[-3mm]
  \end{tabular}\\[3mm]
  \small PLA University of Science and Technology
  \end{center}

  \begin{center}
  Christian Urban\\[0mm]
  \small King's College London
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Why Turing Machines?}%

  \begin{itemize}
  \item At the beginning, it was just a student project
  about computability.\smallskip

  \begin{center}
  \begin{tabular}{c}
  \includegraphics[scale=0.3]{boolos.jpg}\\[-2mm]
  \footnotesize Computability and Logic (5th.~ed)\\[-2mm]
  \footnotesize Boolos, Burgess and Jeffrey\\[2mm]
  \end{tabular}
  \end{center}

  \item found an inconsistency in the definition of halting computations
  (Chap.~3 vs Chap.~8)
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Some Previous Works}%

  \begin{itemize}
  \item Norrish formalised computability theory in HOL starting
  from the lambda-calculus\smallskip 
  \begin{itemize}
  \item \textcolor{gray}{for technical reasons we could not follow his work}
  \item \textcolor{gray}{some proofs use TMs (Wang tilings)}
  \end{itemize}
  \bigskip

  \item Asperti and Ricciotti formalised TMs in Matita\smallskip
  \begin{itemize}
  \item \textcolor{gray}{no undecidability result $\Rightarrow$ interest in complexity}
  \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates}
  \begin{quote}
  \textcolor{gray}{"In particular, the fact that the universal machine operates with a different 
  alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}
  \end{quote}
  \end{itemize}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
  \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
                     draw=black!50, top color=white, bottom color=black!20]
  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
                     draw=red!70, top color=white, bottom color=red!50!black!20]
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{The Big Picture}%

  \begin{center}
  \begin{tikzpicture}
  \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
  { \node (def1)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
    \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
    \node (alg1)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    
  };

  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
  \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
  
  \end{tikzpicture}
  \end{center}

  \only<2->{
  \begin{textblock}{3}(8.3,4.0)
  \begin{tikzpicture}
  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
  \end{tikzpicture}
  \end{textblock}

  \begin{textblock}{3}(3.1,4.0)
  \begin{tikzpicture}
  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
  \end{tikzpicture}
  \end{textblock}}

  \only<3->{
  \begin{textblock}{4}(10.9,9.4)
  \begin{tikzpicture}
  \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
  \end{tikzpicture}
  \end{textblock}

  \begin{textblock}{3}(1,10.0)
  \begin{tikzpicture}
  \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
  \end{tikzpicture}
  \end{textblock}}

  \only<4->{
  \begin{textblock}{4}(4.2,12.4)
  \begin{tikzpicture}
  \draw (0,0) node {\begin{tabular}{l}a correct UTM by translation\end{tabular}};
  \end{tikzpicture}
  \end{textblock}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Turing Machines}%

  \begin{itemize}
  \item tapes are lists and contain @{text 0}s or @{text 1}s only

  \begin{center}
\begin{tikzpicture}[scale=1]
  \draw[very thick] (-3.0,0)   -- ( 3.0,0);
  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 3.0,0)   -- ( 3.0,0.5);
  \draw[very thick] (-3.0,0)   -- (-3.0,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);
  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);
  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);
  \draw[fill]     (-1.65,0.1) rectangle (-1.35,0.4);
  \draw (-0.25,0.8) -- (-0.25,-0.8);
  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
  \node [anchor=base] at (-0.85,-0.5) {\small left list\;\;\;\;\mbox{}};
  \node [anchor=base] at (0.40,-0.5) {\small \mbox{}\;\;\;\;right list};
  \node [anchor=base] at (0.1,0.7) {\small \;\;head};
  \node [anchor=base] at (-2.2,0.2) {\ldots};
  \node [anchor=base] at ( 2.3,0.2) {\ldots};
  \end{tikzpicture}
  \end{center}\pause

  \item @{text steps} function:

  \begin{quote}\rm
  What does the TM calculate after it has executed @{text n} steps?
  \end{quote}\pause

  \item designate the @{text 0}-state as "halting state" and remain there 
  forever, i.e.~have a @{text Nop}-action
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Register Machines}%

  \begin{itemize}
  \item programs are lists of instructions

  \begin{center}
  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
  @{text "I"} & $::=$  & @{term "Goto L\<iota>"}
  & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]
  & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]
  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if the content of @{text R} is non-zero,}\\
  & & & \textcolor{black!60}{then decrement it by one}\\
  & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}
  \end{tabular}
  \end{center}
  \end{itemize}

  \only<2->{
  \begin{textblock}{4}(0.3,11.8)
  \begin{tikzpicture}
  \node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}] 
   at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};
  \end{tikzpicture}
  \end{textblock}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Recursive Functions}%

  \begin{itemize}
  \item[] 
  \begin{center}
  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
  @{text "rec"} & $::=$  & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]
  & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]
  & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]
  & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]
  & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]
  & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}
  \end{tabular}
  \end{center}\bigskip

  \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ 
  can be defined by simple recursion\\ (HOL has @{term "Least"})
  
  \item \small you define
  \begin{itemize}
  \item addition, multiplication, logical operations, quantifiers\ldots
  \item coding of numbers (Cantor encoding), UF
  \end{itemize}

  \end{itemize}
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Copy Turing Machine}%

  \begin{itemize}
  \item TM that copies a number on the input tape
  \begin{center}
  @{text "copy \<equiv> cbegin ; cloop ; cend"}
  \end{center}\smallskip


  \begin{center}
  \begin{tikzpicture}[scale=0.7]
  \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
  \node [anchor=base] at (2.2,-0.8) {\small$\overbrace{@{text cbegin}}^{}$};
  \node [anchor=base] at (5.6,-0.8) {\small$\overbrace{@{text cloop}}^{}$};
  \node [anchor=base] at (10.5,-0.8) {\small$\overbrace{@{text cend}}^{}$};


  \begin{scope}[shift={(0.5,0)}]
  \draw[very thick] (-0.25,0)   -- ( 1.25,0);
  \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \end{scope}

  \begin{scope}[shift={(2.9,0)}]
  \draw[very thick] (-0.25,0)   -- ( 2.25,0);
  \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \end{scope}

  \begin{scope}[shift={(6.8,0)}]
  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \end{scope}

  \begin{scope}[shift={(11.7,0)}]
  \draw[very thick] (-0.75,0)   -- ( 3.25,0);
  \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
  \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);
  \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);
  \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
  \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
  \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);
  \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);
  \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);
  \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
  \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
  \end{scope}
  \end{tikzpicture}
  \end{center}\bigskip

  \footnotesize
  \begin{center}
  \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
  \begin{tabular}[t]{@ {}l@ {}}
  @{text cbegin} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>1\<^esub>, 3), (L, 4),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 
  \end{tabular}
  &
  \begin{tabular}[t]{@ {}l@ {}}
  @{text cloop} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>0\<^esub>, 2), (R, 3), (R, 4),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>1\<^esub>, 5), (R, 4), (L, 6),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 
  \end{tabular}
  &
  \begin{tabular}[t]{@ {}l@ {}}
  @{text cend} @{text "\<equiv>"}\\
  \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>1\<^esub>, 3),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>0\<^esub>, 4), (R, 0),"}\\
  \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 
  \end{tabular}
  \end{tabular}
  \end{center}

  \end{itemize}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  \definecolor{mygrey}{rgb}{.80,.80,.80}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Hoare Logic for TMs}%

  \begin{itemize}
  \item Hoare-triples\onslide<2>{ and Hoare-pairs:}

  \small
  \begin{center}
  \begin{tabular}{@ {\hspace{-6mm}}c@ {\hspace{-3mm}}c@ {}}
  \begin{tabular}[t]{@ {}l@ {}}
  \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
  \hspace{7mm}if @{term "P tp"} holds then\\
  \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
  \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
  \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
  \end{tabular} &

  \onslide<2>{
  \begin{tabular}[t]{@ {}l@ {}}
  \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 
  \hspace{7mm}if @{term "P tp"} holds then\\
  \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
  \end{tabular}}
  \end{tabular}
  \end{center}

  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

(*<*)
lemmas HR1 = 
  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]

lemmas HR2 =
  Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
(*>*)

text_raw {*
  \definecolor{mygrey}{rgb}{.80,.80,.80}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Some Derived Rules}%
  \large
  
  \begin{center}
  @{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\
  
  \begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}
  $\inferrule*
  {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
  {@{thm (concl) HR1}}
  $ &
  $
  \inferrule*
  {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
  {@{thm (concl) HR2}}
  $
  \end{tabular}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[b]
  \frametitle{Undecidability}%

  \begin{textblock}{7}(4,2.4)
  @{thm tcontra_def}
  \end{textblock}
  
  \only<2>{
  \begin{itemize}
  \item Suppose @{text H} decides @{text contra} called with the code 
  of @{text contra} halts, then\smallskip

  \begin{center}\small
  \begin{tabular}{@ {}l@ {}}
  \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
  @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
  @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
  @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
  \end{tabular}\bigskip\bigskip
  \\
  \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
  $\inferrule*{
    \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
    {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
    \\ @{term "{P\<^sub>3} dither \<up>"}
   }
   {@{term "{P\<^sub>1} tcontra \<up>"}}
  $
  \end{tabular}
  \end{tabular}
  \end{center}
  \end{itemize}}
  \only<3>{
  \begin{itemize}
  \item Suppose @{text H} decides @{text contra} called with the code 
  of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}

  \begin{center}\small
  \begin{tabular}{@ {}l@ {}}
  \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
  @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
  @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
  @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
  \end{tabular}\bigskip\bigskip
  \\
  \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
  $\inferrule*{
    \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
    {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
    \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
   }
   {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
  $
  \end{tabular}
  \end{tabular}
  \end{center}
  \end{itemize}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  \definecolor{mygrey}{rgb}{.80,.80,.80}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Hoare Reasoning}%

  \begin{itemize}
  \item reasoning is quite demanding, e.g.~the invariants 
  of the copy-machine:\\[-5mm]\mbox{}

  \footnotesize
  \begin{center}
  \begin{tabular}{@ {\hspace{-5mm}}c@ {}}
  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {\hspace{-0.9cm}}l@ {}}
  \hline
  @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
  @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
  @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
  @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
                                &             & @{thm (rhs) inv_begin02}\smallskip \\
   \hline
  @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
                               &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
  @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
   \hline
  @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
  @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
  \hline
  \end{tabular}
  \end{tabular}
  \end{center}

  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}



text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Midway Conclusion}%

  \begin{itemize}
  \item feels awfully like reasoning about machine code
  \item compositional constructions / reasoning is not at all frictionless
  \item sizes

  \begin{center}
  \begin{tabular}{ll}
  & sizes:\smallskip\\
  UF       & @{text 140843} constructors\\
  URM      & @{text 2} Mio instructions\\
  UTM      & @{text 38} Mio states\\
  \end{tabular}
  \end{center}\smallskip\pause

  \item an observation: our treatment of recursive functions is a mini-version
  of the work by\\ Myreen \& Owens about deeply embedding HOL
  \end{itemize}
 
  \only<1>{
  \begin{textblock}{4}(2,13.9)
  \begin{tikzpicture}
  \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: 
  URM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
  \end{tikzpicture}
  \end{textblock}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%

  \onslide<3->{
  \begin{itemize}
  \item Jensen, Benton, Kennedy ({\bf 2013}),
  {\it High-Level Separation Logic for Low-Level Code}\medskip\\
  
  \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
  PhD thesis\medskip

  \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}

  \end{itemize}}

  \only<2->{
  \begin{textblock}{4}(1.4,0.9)
  \begin{tikzpicture}
  \draw (0,0) node {\fontspec{Chalkduster}\textcolor{red!80}{\LARGE Stealing}};
  \end{tikzpicture}
  \end{textblock}}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Better Composability}%

  \begin{itemize}
  \item an idea from Jensen, Benton \& Kennedy who looked at X86 
  assembly programs and macros\bigskip
  
  \item assembly for TMs:\medskip
  \begin{center}
  \begin{tabular}{l}
  @{text "move_one_left"} @{text "\<equiv>"}\\ 
  \hspace{13mm} @{text "\<Lambda> exit."}\\
  \hspace{16mm} @{text "Inst (L, exit) (L, exit)"} @{text ";"}\\
  \hspace{16mm} @{text "Label exit"}\\
  \end{tabular}
  \end{center}\bigskip\bigskip

  \begin{tabular}{l}
  $\Rightarrow$ represent "state" labels as functions\\
  \phantom{$\Rightarrow$} (with bound variables $\Rightarrow$ locality) 
  \end{tabular}
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Better Composability}%

  \begin{center}
  \begin{tabular}{@ {\hspace{-10mm}}l}
  @{text "move_left_until_zero"} @{text "\<equiv>"} \\
  \hspace{31mm} @{text "\<Lambda> start exit."}\\
  \hspace{36mm} @{text "Label start"} @{text ";"}\\
  \hspace{36mm} @{text "if_zero exit"} @{text ";"}\\
  \hspace{36mm} @{text "move_left"} @{text ";"}\\
  \hspace{36mm} @{text "jmp start"} @{text ";"}\\
  \hspace{36mm} @{text "Label exit"}\\
  \end{tabular}
  \end{center}

  \small
  \begin{tabular}{l}
  @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^sub>0, e), (W\<^sub>1, exit); Label exit"}\\
  \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^sub>0, e), (W\<^sub>1, e)"}
  \end{tabular}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{{\large The Trouble With Hoare-Triples}}%

  \begin{itemize}
  \item Whenever we wanted to prove 

  \begin{center}
  \large @{text "{P} p {Q}"}
  \end{center}\bigskip\medskip
 
  \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}

  
  
  \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates
  \textcolor{gray}{(not easy either)}
  \end{itemize}\pause
  
  \begin{center}
  \alert{very little opportunity for automation}
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Separation Algebra}%

  \begin{itemize}
  \item use some infrastructure introduced by Klein et al in Isabelle/HOL
  \item and an idea by Myreen\bigskip\bigskip

  \begin{center}
  \large @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"}\bigskip\bigskip
  \end{center}
  
  \item[] @{text "p, c, q"} will be assertions in a separation logic\pause

  \begin{center}
  e.g.~~@{text "\<lbrace>st i \<star> hd n \<star> ones u v \<star> zero (v + 1)\<rbrace>"}
  \end{center}
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Separation Triples}%

  \Large
  \begin{center}
  \begin{tabular}{l@ {\hspace{-10mm}}l}
  @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\
  & @{text "\<forall> cf r."}\\
  & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\
  & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"} 
  \end{tabular}
  \end{center}\bigskip\bigskip

  \normalsize
  @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Automation}%

  \begin{itemize}
  \item we introduced some tactics for handling sequential programs\bigskip

  \begin{center}
  @{text "\<lbrace>p\<rbrace> i:[c\<^sub>1 ; ... ; c\<^sub>n]:j \<lbrace>q\<rbrace>"}
  \end{center}\bigskip\bigskip

  \item for loops we often only have to do inductions on the length 
  of the input (e.g.~how many @{text "1"}s are on the tape)\pause
  
  \item these macros allow us to completely get rid of register machines
  \end{itemize}
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Conclusion}%

  \begin{itemize}
  \item What started out as a student project, turned out to be much more
  fun than first thought.\bigskip

  \item Where can you claim that you proved the correctness of
  a @{text "38"} Mio instruction program?
  (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
  \bigskip
  
  \item We learned a lot about current verification technology for low-level code
  (we had no infrastructure: CPU model).\bigskip

  \item The existing literature on TMs \& RMs leave out quite a bit of the story
  (not to mention contains bugs).
  \end{itemize}
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

(*<*)
end
end
(*>*)