(*<*)

theory Paper

imports "../thys/UTM" "../thys/Abacus_Defs"

begin

(*

value "map (steps (1,[],[Oc]) ([(L,0),(L,2),(R,2),(R,0)],0)) [0 ..< 4]"

*)

hide_const (open) s 

hide_const (open) Divides.adjust

abbreviation

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

consts DUMMY::'a

(* Theorems as inference rules from LaTeXsugar.thy *)

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] 48) and

  set ("") and

  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

  update2 ("update") and

  tm_wf0 ("wf") and

  tcopy_begin ("cbegin") and

  tcopy_loop ("cloop") and

  tcopy_end ("cend") and

  step0 ("step") and

  tcontra ("contra") and

  code_tcontra ("code contra") and

  steps0 ("steps") and

  adjust0 ("adjust") and

  exponent ("_\<^bsup>_\<^esup>") and

  tcopy ("copy") and 

  tape_of ("\<langle>_\<rangle>") and 

  tm_comp ("_ ; _") and 

  DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") 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") and

  measure_begin_step ("M\<^bsub>cbegin\<^esub>") and

  layout_of ("layout") and

  findnth ("find'_nth") and

  recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and

  Pr ("Pr\<^isup>_") and

  Cn ("Cn\<^isup>_") and

  Mn ("Mn\<^isup>_") and

  rec_exec ("eval") and

  tm_of_rec ("translate") and

  listsum ("\<Sigma>")

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)

declare [[show_question_marks = false]]

lemma nats2tape:

  shows "<([]::nat list)> = []"

  and "<[n]> = <n>"

  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"

  and "<(n, m)> = <n> @ [Bk] @ <m>"

  and "<[n, m]> = <(n, m)>"

  and "<n> = Oc \<up> (n + 1)" 

apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)

apply(case_tac ns)

apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)

done 

lemmas HR1 = 

  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]

lemmas HR2 =

  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]

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

lemma layout:

  shows "layout_of [] = []"

  and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"

  and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"

  and   "layout_of ((Goto l)#is) = 1#(layout_of is)"

by(auto simp add: layout_of.simps length_of.simps)

lemma adjust_simps:

  shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"

by(simp add: adjust.simps)

fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

  where

  "clear n e = [Dec n e, Goto 0]"

partial_function (tailrec)

  run

where

  "run p cf = (if (is_final cf) then cf else run p (step0 cf p))"

lemma numeral2:

  shows "11 = Suc 10"

  and   "12 = Suc 11"

  and   "13 = Suc 12"

  and   "14 = Suc 13"

  and   "15 = Suc 14"

apply(arith)+

done

(*

lemma "run tcopy (1, [], <0::nat>) = (0, [Bk], [Oc, Bk, Oc])"

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral nth_of.simps del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)

apply(simp only: numeral[symmetric])

apply(simp)

apply(subst run.simps)

apply(simp)

done

*)

(*>*)

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. 

%Suppose you want to mechanise a proof for whether a predicate @{term P}, 

%say, is decidable or not. Decidability of @{text P} usually

%amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this

%does \emph{not} work in 

%Since Isabelle/HOL and other HOL theorem provers,

%are 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. We hit on

%this limitation previously when we mechanised the correctness proofs

%of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but

%were unable to formalise arguments about decidability or undecidability.

%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.

\noindent

The motivation of this paper is to bring the ability to reason

about results from computability theory, for example decidability of the halting problem,

to the theorem prover Isabelle/HOL.  Norrish formalised computability

theory in HOL4. He choose the $\lambda$-calculus as the starting point

for his formalisation 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 \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 Turing machine

programs (similarly abacus programs) can be completely

\emph{unstructured}, behaving similar to Basic programs containing the

infamous goto \cite{Dijkstra68}. This precludes in the general case a

compositional Hoare-style reasoning about Turing programs.  We provide

such Hoare-rules for when it \emph{is} possible to reason in a

compositional manner (which is fortunately quite often), but also

tackle the more complicated case when we translate abacus programs

into Turing programs.  This reasoning about concrete Turing machine

programs is usually left out in the informal literature,

e.g.~\cite{Boolos87}.

%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: we are aware of

the 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. However, they do

\emph{not} formalise the undecidability of the halting problem since

their main focus is complexity, rather than computability theory. They

also report that the informal proofs from which they started are not

``sufficiently accurate to be directly usable as a guideline for

formalization'' \cite[Page 2]{AspertiRicciotti12}. For our

formalisation we follow mainly the proofs from the textbook by Boolos

et al \cite{Boolos87} and found that the description there is quite

detailed. Some details are left out however: for example, constructing

the \emph{copy Turing machine} is left as an exercise to the

reader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}

only shows 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. 

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 translating abacus machines to Turing machines and in

turn recursive functions to abacus machines. The universal Turing

machine can then be constructed by translating from a recursive function. 

The part of mechanising the translation of recursive function to register 

machines has already been done by Zammit in HOL \cite{Zammit99}, 

although his register machines use a slightly different instruction

set than the one described in \cite{Boolos87}.

\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.  For reasoning about Turing

machine programs we derive Hoare-rules.  We also construct the

universal Turing machine from \cite{Boolos87} by translating recursive

functions to abacus machines and abacus machines to Turing

machines. This works essentially like a small, verified compiler 

from recursive functions to Turing machine programs.

When formalising the universal Turing machine,

we stumbled in \cite{Boolos87} upon an inconsistent use of the definition of

what partial function a Turing machine calculates. 

%Since we have set up in

%Isabelle/HOL a very general computability model and undecidability

%result, we are able to formalise other results: we describe a proof of

%the computational equivalence of single-sided Turing machines, which

%is not given in \cite{Boolos87}, but needed for example for

%formalising the undecidability proof of Wang's tiling problem

%\cite{Robinson71}.  %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 \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 use

  the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists

  composed of @{term n} elements of @{term Bk}s.  We also 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

  scans. This can be pictured as follows:

  %

  \begin{center}

  \begin{tikzpicture}[scale=0.9]

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

  \node [anchor=base] at (0.40,-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};