(*<*)

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 (latex output)

  Oc ("1") and

  Bk ("0") 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_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")

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]

  \end{tabular}}

  \begin{center}

  \end{center}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \begin{itemize}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \begin{itemize}

  \end{itemize}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Turing Machines}%

  \begin{itemize}

  \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[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}

  \end{quote}\pause

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Copy Turing Machines}%

  \begin{itemize}

  \item TM that copies a number on the input tape

  \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$};

  \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 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} &

  \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}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  \definecolor{mygrey}{rgb}{.80,.80,.80}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Hoare Reasoning}%

  \begin{itemize}

  \footnotesize

  \begin{center}

  \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{center}

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Recursive Functions}%

  \begin{itemize}

  \item addition, multiplication, \ldots

  \item logical operations, quantifiers\ldots

  \item coding of numbers (Cantor encoding)

  \item UF\pause\bigskip

  \item Recursive Functions $\Rightarrow$ Register Machines

  \item Register Machines $\Rightarrow$ Turing Machines

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Sizes}%

  \begin{itemize}

  \end{itemize}\bigskip\bigskip

  \small

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \mode<presentation>{

  \begin{frame}[c]

  \frametitle{Separation Algebra}%

  \begin{itemize}

  \item introduced a separation algebra framework for register machines and TMs 

  \item we can semi-automate the reasoning for our small TMs

  \item we can assemble bigger programs out of smaller components\bigskip

  \item looks awfully like ``real'' assembly code\pause

  \item Conclusion: we have a playing ground for reasoning about low-level 

  code; we work on automation

  \end{itemize}

  \end{frame}}

  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

(*<*)

end

(*>*)