# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1385213033 0
# Node ID 447b433b67facbba191101add9e4515561a03fd8
# Parent  a21fb87bb0bdca8a628bd18940ebe7b6e43b3bed
added things --- in messy state

diff -r a21fb87bb0bd -r 447b433b67fa ROOT
--- a/ROOT	Tue Sep 03 15:02:52 2013 +0100
+++ b/ROOT	Sat Nov 23 13:23:53 2013 +0000
@@ -1,5 +1,5 @@
 session UTM = HOL +
-  options [document = false]
+  options [quick_and_dirty, document = false]
   theories
     "thys/Turing"
     "thys/Turing_Hoare"
@@ -37,3 +37,11 @@
     "Slides2"
   files
     "document/root.tex"
+
+
+session Slides3 in Slides = UTM +
+  options [quick_and_dirty, document = pdf, document_output = "..", document_variants = "slides3"]
+  theories
+    "Slides3"
+  files
+    "document/root.tex"
\ No newline at end of file
diff -r a21fb87bb0bd -r 447b433b67fa Slides/Slides1.thy
--- a/Slides/Slides1.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/Slides/Slides1.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -15,16 +15,16 @@
   Oc ("0") and
   Bk ("1") and
   exponent ("_\<^bsup>_\<^esup>") and
-  inv_begin0 ("I\<^isub>0") and
-  inv_begin1 ("I\<^isub>1") and
-  inv_begin2 ("I\<^isub>2") and
-  inv_begin3 ("I\<^isub>3") and
-  inv_begin4 ("I\<^isub>4") 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\<^isub>1") and
-  inv_loop0 ("J\<^isub>0") and
-  inv_end1 ("K\<^isub>1") and
-  inv_end0 ("K\<^isub>0")
+  inv_loop1 ("J\<^sub>1") and
+  inv_loop0 ("J\<^sub>0") and
+  inv_end1 ("K\<^sub>1") and
+  inv_end0 ("K\<^sub>0")
 
 
  
diff -r a21fb87bb0bd -r 447b433b67fa Slides/Slides2.thy
--- a/Slides/Slides2.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/Slides/Slides2.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -49,20 +49,20 @@
   Oc ("1") and
   Bk ("0") and
   exponent ("_\<^bsup>_\<^esup>" [107] 109) and
-  inv_begin0 ("I\<^isub>0") and
-  inv_begin1 ("I\<^isub>1") and
-  inv_begin2 ("I\<^isub>2") and
-  inv_begin3 ("I\<^isub>3") and
-  inv_begin4 ("I\<^isub>4") 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\<^isub>1") and
-  inv_loop0 ("J\<^isub>0") and
-  inv_end1 ("K\<^isub>1") and
-  inv_end0 ("K\<^isub>0") and
-  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
-  Pr ("Pr\<^isup>_") and
-  Cn ("Cn\<^isup>_") and
-  Mn ("Mn\<^isup>_") 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 
@@ -563,10 +563,10 @@
 
 (*<*)
 lemmas HR1 = 
-  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  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\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
 (*>*)
 
 text_raw {*
@@ -615,18 +615,18 @@
   \begin{center}\small
   \begin{tabular}{@ {}l@ {}}
   \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
-  @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+  @{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\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
-    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
-    \\ @{term "{P\<^isub>3} dither \<up>"}
+    \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\<^isub>1} tcontra \<up>"}}
+   {@{term "{P\<^sub>1} tcontra \<up>"}}
   $
   \end{tabular}
   \end{tabular}
@@ -640,18 +640,18 @@
   \begin{center}\small
   \begin{tabular}{@ {}l@ {}}
   \begin{tabular}[t]{@ {\hspace{-1mm}}l@ {}}
-  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+  @{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\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
-    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
-    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+    \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\<^isub>1} tcontra {Q\<^isub>3}"}}
+   {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
   $
   \end{tabular}
   \end{tabular}
@@ -818,8 +818,8 @@
 
   \small
   \begin{tabular}{l}
-  @{text "if_zero e \<equiv> \<Lambda> exit. Inst (W\<^isub>0, e), (W\<^isub>1, exit); Label exit"}\\
-  \hspace{5mm}@{text "jmp e \<equiv> Inst (W\<^isub>0, e), (W\<^isub>1, e)"}
+  @{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}}
@@ -913,7 +913,7 @@
   \item we introduced some tactics for handling sequential programs\bigskip
 
   \begin{center}
-  @{text "\<lbrace>p\<rbrace> i:[c\<^isub>1 ; ... ; c\<^isub>n]:j \<lbrace>q\<rbrace>"}
+  @{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 
diff -r a21fb87bb0bd -r 447b433b67fa Slides/Slides3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides3.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -0,0 +1,960 @@
+(*<*)
+theory Slides3
+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
+(*>*)
\ No newline at end of file
diff -r a21fb87bb0bd -r 447b433b67fa thys/Abacus.thy
--- a/thys/Abacus.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/Abacus.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -546,9 +546,11 @@
 lemma compile_mod2: "length (concat (take n (tms_of ap))) mod 2 = 0"
 apply(induct n, auto)
 apply(case_tac "n < length (tms_of ap)", simp add: take_Suc_conv_app_nth, auto)
-apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
+(*apply(subgoal_tac "length (tms_of ap ! n) mod 2 = 0")
 apply arith
 by auto
+*)
+done
 
 lemma tpa_states:
   "\<lbrakk>tp = concat (take as (tms_of ap));
diff -r a21fb87bb0bd -r 447b433b67fa thys/Recursive.thy
--- a/thys/Recursive.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/Recursive.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -2786,9 +2786,13 @@
 lemma wf_tm_from_abacus: 
   "tp = tm_of ap \<Longrightarrow> 
     tm_wf (tp @ shift( mopup n) (length tp div 2), 0)"
-  using length_start_of_tm[of ap] all_le_start_of[of ap]
+ using length_start_of_tm[of ap] all_le_start_of[of ap]
 apply(auto simp: tm_wf.simps List.list_all_iff)
-done
+apply(case_tac n)
+apply(simp add: mopup.simps)
+apply(simp add: mopup.simps)
+apply (metis mod_mult_right_eq mod_mult_self2 mod_mult_self2_is_0 mult_2_right nat_mult_commute numeral_Bit0)
+sorry
 
 lemma wf_tm_from_recf:
   assumes compile: "tp = tm_of_rec recf"
diff -r a21fb87bb0bd -r 447b433b67fa thys/UTM.thy
--- a/thys/UTM.thy	Tue Sep 03 15:02:52 2013 +0100
+++ b/thys/UTM.thy	Sat Nov 23 13:23:53 2013 +0000
@@ -1439,7 +1439,7 @@
 apply(simp add: t_twice_def t_twice_compile_def)
 using mopup_mod2[of 1]
 apply(simp)
-by arith
+done
 
 lemma wcode_jump1: 
   "\<exists> stp ln rn. steps0 (Suc (t_twice_len) + length t_wcode_main_first_part div 2,
@@ -2069,7 +2069,7 @@
 
 lemma [intro]: "length t_twice mod 2 = 0"
 apply(auto simp: t_twice_def t_twice_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma t_fourtimes_append_pre:
   "steps0 (Suc 0, Bk # Bk # ires, Oc\<up>(Suc rs) @ Bk\<up>(n)) t_fourtimes stp
@@ -2131,11 +2131,11 @@
 
 lemma even_twice_len: "length t_twice mod 2 = 0"
 apply(auto simp: t_twice_def t_twice_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma even_fourtimes_len: "length t_fourtimes mod 2 = 0"
 apply(auto simp: t_fourtimes_def t_fourtimes_compile_def)
-done
+by (metis mopup_mod2)
 
 lemma [simp]: "2 * (length t_twice div 2) = length t_twice"
 using even_twice_len