
diff -r 251e192339b7 -r 559e5c6e5113 Paper.thy
--- a/Paper.thy	Thu Jan 17 11:51:00 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,684 +0,0 @@
-(*<*)
-theory Paper
-imports UTM
-begin
-
-hide_const (open) s 
-
-abbreviation 
-  "update p a == new_tape a p"
-
-lemma fetch_def2: 
-  shows "fetch p 0 b == (Nop, 0)"
-  and "fetch p (Suc s) Bk == 
-     (case nth_of p (2 * s) of
-        Some i \<Rightarrow> i
-      | None \<Rightarrow> (Nop, 0))"
-  and "fetch p (Suc s) Oc == 
-     (case nth_of p ((2 * s) + 1) of
-         Some i \<Rightarrow> i
-       | None \<Rightarrow> (Nop, 0))"
-apply -
-apply(rule_tac [!] eq_reflection)
-by (auto split: block.splits simp add: fetch.simps)
-
-lemma new_tape_def2: 
-  shows "new_tape W0 (l, r) == (l, Bk#(tl r))" 
-  and "new_tape W1 (l, r) == (l, Oc#(tl r))"
-  and "new_tape L (l, r) == 
-     (if l = [] then ([], Bk#r) else (tl l, (hd l) # r))" 
-  and "new_tape R (l, r) ==
-     (if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))" 
-  and "new_tape Nop (l, r) == (l, r)"
-apply -
-apply(rule_tac [!] eq_reflection)
-apply(auto split: taction.splits simp add: new_tape.simps)
-done
-
-
-abbreviation 
-  "read r == if (r = []) then Bk else hd r"
-
-lemma tstep_def2:
-  shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))"
-apply -
-apply(rule_tac [!] eq_reflection)
-by (auto split: if_splits prod.split list.split simp add: tstep.simps)
-
-abbreviation
- "run p inp out == \<exists>n. steps (1, inp) p n = (0, out)"
-
-lemma haltP_def2:
-  "haltP p n = (\<exists>k l m. 
-     run p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
-unfolding haltP_def 
-apply(auto)
-done
-
-lemma tape_of_nat_list_def2:
-  shows "tape_of_nat_list [] = []" 
-  and "tape_of_nat_list [n] = exponent Oc (n+1)"
-  and "ns\<noteq> [] ==> tape_of_nat_list (n#ns) = (exponent Oc (n+1)) @ [Bk] @ (tape_of_nat_list ns)"
-apply(auto simp add: tape_of_nat_list.simps)
-apply(case_tac ns)
-apply(auto simp add: tape_of_nat_list.simps)
-done
-
-lemma tshift_def2:
-  fixes p::"tprog"
-  shows "tshift p n == (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
-apply(rule eq_reflection)
-apply(auto simp add: tshift.simps)
-done
-
-lemma change_termi_state_def2:
- "change_termi_state p  == 
-  (map (\<lambda> (a, s). (a, if s = 0 then ((length p) div 2) + 1 else s)) p)"
-apply(rule eq_reflection)
-apply(auto simp add: change_termi_state.simps)
-done
-
-
-
-consts DUMMY::'a
-
-notation (latex output)
-  Cons ("_::_" [78,77] 73) and
-  set ("") and
-  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
-  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
-  t_correct ("twf") and 
-  tstep ("step") and
-  steps ("nsteps") and
-  abc_lm_v ("lookup") and
-  abc_lm_s ("set") and
-  haltP ("stdhalt") and 
-  tshift ("shift") and 
-  tcopy ("copy") and 
-  change_termi_state ("adjust") and
-  tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 
-  t_add ("_ \<oplus> _") and 
-  DUMMY  ("\<^raw:\mbox{$\_$}>")
-
-declare [[show_question_marks = false]]
-(*>*)
-
-section {* Introduction *}
-
-text {*
-
-\noindent
-We formalised in earlier work the correctness proofs for two
-algorithms in Isabelle/HOL---one about type-checking in
-LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
-in access control~\cite{WuZhangUrban12}.  The formalisations
-uncovered a gap in the informal correctness proof of the former and
-made us realise that important details were left out in the informal
-model for the latter. However, in both cases we were unable to
-formalise in Isabelle/HOL computability arguments about the
-algorithms. The reason is that both algorithms are formulated in terms
-of inductive predicates. Suppose @{text "P"} stands for one such
-predicate.  Decidability of @{text P} usually amounts to showing
-whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
-in Isabelle/HOL, since it is a theorem prover based on classical logic
-where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
-is always provable no matter whether @{text P} is constructed by
-computable means. The same problem would arise if we had formulated
-the algorithms as recursive functions, because internally in
-Isabelle/HOL, like in all HOL-based theorem provers, functions are
-represented as inductively defined predicates too.
-
-The only satisfying way out of this problem in a theorem prover based on classical
-logic is to formalise a theory of computability. Norrish provided such
-a formalisation for the HOL4 theorem prover. He choose the
-$\lambda$-calculus as the starting point for his formalisation
-of computability theory,
-because of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his
-formalisation is a clever infrastructure for reducing
-$\lambda$-terms. He also established the computational equivalence
-between the $\lambda$-calculus and recursive functions.  Nevertheless he
-concluded that it would be ``appealing'' to have formalisations for more
-operational models of computations, such as Turing machines or register
-machines.  One reason is that many proofs in the literature use 
-them.  He noted however that in the context of theorem provers
-\cite[Page 310]{Norrish11}:
-
-\begin{quote}
-\it``If register machines are unappealing because of their 
-general fiddliness, Turing machines are an even more 
-daunting prospect.''
-\end{quote}
-
-\noindent
-In this paper we take on this daunting prospect and provide a
-formalisation of Turing machines, as well as abacus machines (a kind
-of register machines) and recursive functions. To see the difficulties
-involved with this work, one has to understand that interactive
-theorem provers, like Isabelle/HOL, are at their best when the
-data-structures at hand are ``structurally'' defined, like lists,
-natural numbers, regular expressions, etc. Such data-structures come
-with convenient reasoning infrastructures (for example induction
-principles, recursion combinators and so on).  But this is \emph{not}
-the case with Turing machines (and also not with register machines):
-underlying their definitions are sets of states together with 
-transition functions, all of which are not structurally defined.  This
-means we have to implement our own reasoning infrastructure in order
-to prove properties about them. This leads to annoyingly fiddly
-formalisations.  We noticed first the difference between both,
-structural and non-structural, ``worlds'' when formalising the
-Myhill-Nerode theorem, where regular expressions fared much better
-than automata \cite{WuZhangUrban11}.  However, with Turing machines
-there seems to be no alternative if one wants to formalise the great
-many proofs from the literature that use them.  We will analyse one
-example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
-standard proof of this property uses the notion of universal
-Turing machines.
-
-We are not the first who formalised Turing machines in a theorem
-prover: we are aware of the preliminary work by Asperti and Ricciotti
-\cite{AspertiRicciotti12}. They describe a complete formalisation of
-Turing machines in the Matita theorem prover, including a universal
-Turing machine. They report that the informal proofs from which they
-started are \emph{not} ``sufficiently accurate to be directly usable as a
-guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we followed mainly the proofs from the textbook
-\cite{Boolos87} and found that the description there is quite
-detailed. Some details are left out however: for example, it is only
-shown how the universal Turing machine is constructed for Turing
-machines computing unary functions. We had to figure out a way to
-generalise this result to $n$-ary functions. Similarly, when compiling
-recursive functions to abacus machines, the textbook again only shows
-how it can be done for 2- and 3-ary functions, but in the
-formalisation we need arbitrary functions. But the general ideas for
-how to do this are clear enough in \cite{Boolos87}. However, one
-aspect that is completely left out from the informal description in
-\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
-machines are correct. We will introduce Hoare-style proof rules
-which help us with such correctness arguments of Turing machines.
-
-The main difference between our formalisation and the one by Asperti
-and Ricciotti is that their universal Turing machine uses a different
-alphabet than the machines it simulates. They write \cite[Page
-23]{AspertiRicciotti12}:
-
-\begin{quote}\it
-``In particular, the fact that the universal machine operates with a
-different alphabet with respect to the machines it simulates is
-annoying.'' 
-\end{quote}
-
-\noindent
-In this paper we follow the approach by Boolos et al \cite{Boolos87},
-which goes back to Post \cite{Post36}, where all Turing machines
-operate on tapes that contain only \emph{blank} or \emph{occupied} cells
-(represented by @{term Bk} and @{term Oc}, respectively, in our
-formalisation). Traditionally the content of a cell can be any
-character from a finite alphabet. Although computationally equivalent,
-the more restrictive notion of Turing machines in \cite{Boolos87} makes
-the reasoning more uniform. In addition some proofs \emph{about} Turing
-machines are simpler.  The reason is that one often needs to encode
-Turing machines---consequently if the Turing machines are simpler, then the coding
-functions are simpler too. Unfortunately, the restrictiveness also makes
-it harder to design programs for these Turing machines. In order
-to construct a universal Turing machine we therefore do not follow 
-\cite{AspertiRicciotti12}, instead follow the proof in
-\cite{Boolos87} by relating abacus machines to Turing machines and in
-turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed as a recursive function.
-
-\smallskip
-\noindent
-{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
-description of Boolos et al \cite{Boolos87} where tapes only have blank or
-occupied cells. We mechanise the undecidability of the halting problem and
-prove the correctness of concrete Turing machines that are needed
-in this proof; such correctness proofs are left out in the informal literature.  
-We construct the universal Turing machine from \cite{Boolos87} by
-relating recursive functions to abacus machines and abacus machines to
-Turing machines. Since we have set up in Isabelle/HOL a very general computability
-model and undecidability result, we are able to formalise the
-undecidability of Wang's tiling problem. We are not aware of any other
-formalisation of a substantial undecidability problem.
-*}
-
-section {* Turing Machines *}
-
-text {* \noindent
-  Turing machines can be thought of as having a read-write-unit, also
-  referred to as \emph{head},
-  ``gliding'' over a potentially infinite tape. Boolos et
-  al~\cite{Boolos87} only consider tapes with cells being either blank
-  or occupied, which we represent by a datatype having two
-  constructors, namely @{text Bk} and @{text Oc}.  One way to
-  represent such tapes is to use a pair of lists, written @{term "(l,
-  r)"}, where @{term l} stands for the tape on the left-hand side of the
-  head and @{term r} for the tape on the right-hand side. We have the
-  convention that the head, abbreviated @{term hd}, of the right-list is
-  the cell on which the head of the Turing machine currently operates. This can
-  be pictured as follows:
-
-  \begin{center}
-  \begin{tikzpicture}
-  \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 (-0.25,0.8) -- (-0.25,-0.8);
-  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
-  \node [anchor=base] at (-0.8,-0.5) {\small left list};
-  \node [anchor=base] at (0.35,-0.5) {\small 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}
-  
-  \noindent
-  Note that by using lists each side of the tape is only finite. The
-  potential infinity is achieved by adding an appropriate blank or occupied cell 
-  whenever the head goes over the ``edge'' of the tape. To 
-  make this formal we define five possible \emph{actions} 
-  the Turing machine can perform:
-
-  \begin{center}
-  \begin{tabular}{rcll}
-  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\
-  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
-  & $\mid$ & @{term L} & move left\\
-  & $\mid$ & @{term R} & move right\\
-  & $\mid$ & @{term Nop} & do-nothing operation\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  We slightly deviate
-  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
-  will become important when we formalise halting computations and also universal Turing 
-  machines. Given a tape and an action, we can define the
-  following tape updating function:
-
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\
-  @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\
-  @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
-  @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
-  @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  The first two clauses replace the head of the right-list
-  with a new @{term Bk} or @{term Oc}, respectively. To see that
-  these two clauses make sense in case where @{text r} is the empty
-  list, one has to know that the tail function, @{term tl}, is defined in
-  Isabelle/HOL
-  such that @{term "tl [] == []"} holds. The third clause 
-  implements the move of the head one step to the left: we need
-  to test if the left-list @{term l} is empty; if yes, then we just prepend a 
-  blank cell to the right-list; otherwise we have to remove the
-  head from the left-list and prepend it to the right-list. Similarly
-  in the fourth clause for a right move action. The @{term Nop} operation
-  leaves the the tape unchanged (last clause).
-
-  Note that our treatment of the tape is rather ``unsymmetric''---we
-  have the convention that the head of the right-list is where the
-  head is currently positioned. Asperti and Ricciotti
-  \cite{AspertiRicciotti12} also considered such a representation, but
-  dismiss it as it complicates their definition for \emph{tape
-  equality}. The reason is that moving the head one step to
-  the left and then back to the right might change the tape (in case
-  of going over the ``edge''). Therefore they distinguish four types
-  of tapes: one where the tape is empty; another where the head
-  is on the left edge, respectively right edge, and in the middle
-  of the tape. The reading, writing and moving of the tape is then
-  defined in terms of these four cases.  In this way they can keep the
-  tape in a ``normalised'' form, and thus making a left-move followed
-  by a right-move being the identity on tapes. Since we are not using
-  the notion of tape equality, we can get away with the unsymmetric
-  definition above, and by using the @{term update} function
-  cover uniformly all cases including corner cases.
-
-  Next we need to define the \emph{states} of a Turing machine.  Given
-  how little is usually said about how to represent them in informal
-  presentations, it might be surprising that in a theorem prover we
-  have to select carefully a representation. If we use the naive
-  representation where a Turing machine consists of a finite set of
-  states, then we will have difficulties composing two Turing
-  machines: we would need to combine two finite sets of states,
-  possibly renaming states apart whenever both machines share
-  states.\footnote{The usual disjoint union operation in Isabelle/HOL
-  cannot be used as it does not preserve types.} This renaming can be
-  quite cumbersome to reason about. Therefore we made the choice of
-  representing a state by a natural number and the states of a Turing
-  machine will always consist of the initial segment of natural
-  numbers starting from @{text 0} up to the number of states of the
-  machine. In doing so we can compose two Turing machine by
-  shifting the states of one by an appropriate amount to a higher
-  segment and adjusting some ``next states'' in the other.
-
-  An \emph{instruction} @{term i} of a Turing machine is a pair consisting of 
-  an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
-  machine is then a list of such pairs. Using as an example the following Turing machine
-  program, which consists of four instructions
-
-  \begin{equation}
-  \begin{tikzpicture}
-  \node [anchor=base] at (0,0) {@{thm dither_def}};
-  \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
-  \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
-  \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
-  \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
-  \end{tikzpicture}
-  \label{dither}
-  \end{equation}
-
-  \noindent
-  the reader can see we have organised our Turing machine programs so
-  that segments of two belong to a state. The first component of the
-  segment determines what action should be taken and which next state
-  should be transitioned to in case the head reads a @{term Bk};
-  similarly the second component determines what should be done in
-  case of reading @{term Oc}. We have the convention that the first
-  state is always the \emph{starting state} of the Turing machine.
-  The zeroth state is special in that it will be used as the
-  ``halting state''.  There are no instructions for the @{text
-  0}-state, but it will always perform a @{term Nop}-operation and
-  remain in the @{text 0}-state.  Unlike Asperti and Riccioti
-  \cite{AspertiRicciotti12}, we have chosen a very concrete
-  representation for programs, because when constructing a universal
-  Turing machine, we need to define a coding function for programs.
-  This can be easily done for our programs-as-lists, but is more
-  difficult for the functions used by Asperti and Ricciotti.
-
-  Given a program @{term p}, a state
-  and the cell being read by the head, we need to fetch
-  the corresponding instruction from the program. For this we define 
-  the function @{term fetch}
- 
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  \multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\
-  @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\
-  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
-  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\
-  @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\
-  \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\
-  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
-  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  In this definition the function @{term nth_of} returns the @{text n}th element
-  from a list, provided it exists (@{term Some}-case), or if it does not, it
-  returns the default action @{term Nop} and the default state @{text 0} 
-  (@{term None}-case). In doing so we slightly deviate from the description
-  in \cite{Boolos87}: if their Turing machines transition to a non-existing
-  state, then the computation is halted. We will transition in such cases
-  to the @{text 0}-state. However, with introducing the
-  notion of \emph{well-formed} Turing machine programs we will later exclude such
-  cases and make the  @{text 0}-state the only ``halting state''. A program 
-  @{term p} is said to be well-formed if it satisfies
-  the following three properties:
-
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
-                        & @{text "\<and>"} & @{term "iseven (length p)"}\\
-                        & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  The first says that @{text p} must have at least an instruction for the starting 
-  state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 
-  state, and the third that every next-state is one of the states mentioned in
-  the program or being the @{text 0}-state.
-
-  A \emph{configuration} @{term c} of a Turing machine is a state together with 
-  a tape. This is written as @{text "(s, (l, r))"}. If we have a 
-  configuration and a program, we can calculate
-  what the next configuration is by fetching the appropriate action and next state
-  from the program, and by updating the state and tape accordingly. 
-  This single step of execution is defined as the function @{term tstep}
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\
-  \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
-  \hspace{10mm}@{text "in (s', update (l, r) a)"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
-  empty it returns @{term Bk}.
-  It is impossible in Isabelle/HOL to lift the @{term step}-function realising
-  a general evaluation function for Turing machines. The reason is that functions in HOL-based
-  provers need to be terminating, and clearly there are Turing machine 
-  programs that are not. We can however define an evaluation
-  function so that it performs exactly @{text n} steps:
-
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
-  @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  Recall our definition of @{term fetch} with the default value for
-  the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 
-  then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
-  does not actually halt, but rather transitions to the @{text 0}-state and 
-  remains there performing @{text Nop}-actions until @{text n} is reached. 
-
-  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
-  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
-  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  where @{text 1} stands for the starting state and @{text 0} for our final state.
-  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
-
-  \begin{center}
-  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
-  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
-  \end{center}
-
-  \noindent
-  Later on we need to consider specific Turing machines that 
-  start with a tape in standard form and halt the computation
-  in standard form. To define a tape in standard form, it is
-  useful to have an operation @{term "tape_of_nat_list DUMMY"} that 
-  translates 
-  lists of natural numbers into tapes. 
-
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(1)}\\
-  @{thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(2)}\\
-  @{thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(3)}\\
-  \end{tabular}
-  \end{center}
-
-  
-
-
-  By this we mean
-
-  \begin{center}
-  @{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
-  \end{center}
-
-  \noindent
-  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
-  and the head pointing to the first one; the Turing machine
-  halts with a tape consisting of some @{term Bk}s, followed by a 
-  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
-  The head in the output is pointing again at the first @{term Oc}.
-  The intuitive meaning of this definition is to start the Turing machine with a
-  tape corresponding to a value @{term n} and producing
-  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
-  clustered on the output tape).
-
-  Before we can prove the undecidability of the halting problem for Turing machines, 
-  we have to define how to compose two Turing machines. Given our setup, this is 
-  relatively straightforward, if slightly fiddly. We use the following two
-  auxiliary functions:
-
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\
-  \hspace{4mm}@{thm (rhs) tshift_def2}\\
-  @{thm (lhs) change_termi_state_def2} @{text "\<equiv>"}\\
-  \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\
-  \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  The first adds @{text n} to all states, exept the @{text 0}-state,
-  thus moving all ``regular'' states to the segment starting at @{text
-  n}; the second adds @{term "length p div 2 + 1"} to the @{text
-  0}-state, thus ridirecting all references to the ``halting state''
-  to the first state after the program @{text p}.  With these two
-  functions in place, we can define the \emph{sequential composition}
-  of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
-
-  \begin{center}
-  @{thm t_add.simps[where ?t1.0="p\<^isub>1" and ?t2.0="p\<^isub>2", THEN eq_reflection]}
-  \end{center}
-
-  \noindent
-  This means @{text "p\<^isub>1"} is executed first. Whenever it originally
-  transitioned to the @{text 0}-state, it will in the composed program transition to the starting
-  state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
-  have been shifted in order to make sure that the states of the composed 
-  program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 
-  an initial segment of the natural numbers.
-
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
-  @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
-  \end{tabular}
-  \end{center}
-
-
-  assertion holds for all tapes
-
-  Hoare rule for composition
-
-  For showing the undecidability of the halting problem, we need to consider
-  two specific Turing machines. copying TM and dithering TM
-
-  correctness of the copying TM
-
-  measure for the copying TM, which we however omit.
-
-  halting problem
-*}
-
-section {* Abacus Machines *}
-
-text {*
-  \noindent
-  Boolos et al \cite{Boolos87} use abacus machines as a 
-  stepping stone for making it less laborious to write
-  programs for Turing machines. Abacus machines operate
-  over an unlimited number of registers $R_0$, $R_1$, \ldots
-  each being able to hold an arbitrary large natural number.
-  We use natural numbers to refer to registers, but also
-  to refer to \emph{opcodes} of abacus 
-  machines. Obcodes are given by the datatype
-
-  \begin{center}
-  \begin{tabular}{rcll}
-  @{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\
-  & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
-  & & & then decrement it by one\\
-  & & & otherwise jump to opcode $o$\\
-  & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  A \emph{program} of an abacus machine is a list of such
-  obcodes. For example the program clearing the register
-  $R$ (setting it to 0) can be defined as follows:
-
-  \begin{center}
-  @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
-  \end{center}
-
-  \noindent
-  The second opcode @{term "Goto 0"} in this programm means we 
-  jump back to the first opcode, namely @{text "Dec R o"}.
-  The \emph{memory} $m$ of an abacus machine holding the values
-  of the registers is represented as a list of natural numbers.
-  We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
-  which looks up the content of register $R$; if $R$
-  is not in this list, then we return 0. Similarly we
-  have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
-  sets the value of $R$ to $n$, and if $R$ was not yet in $m$
-  it pads it approriately with 0s.
-
-
-  Abacus machine halts when it jumps out of range.
-*}
-
-
-section {* Recursive Functions *}
-
-section {* Wang Tiles\label{Wang} *}
-
-text {*
-  Used in texture mapings - graphics
-*}
-
-
-section {* Related Work *}
-
-text {*
-  The most closely related work is by Norrish \cite{Norrish11}, and Asperti and 
-  Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on 
-  lambda-terms. For this he introduced a clever rewriting technology
-  based on combinators and de-Bruijn indices for
-  rewriting modulo $\beta$-equivalence (to keep it manageable)
-*}
-
-
-(*
-Questions:
-
-Can this be done: Ackerman function is not primitive 
-recursive (Nora Szasz)
-
-Tape is represented as two lists (finite - usually infinite tape)?
-
-*)
-
-
-(*<*)
-end
-(*>*)
\ No newline at end of file




