(*<*)

theory Paper

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

begin

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 ("_ \<oplus> _") 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_calc_rel ("eval") and 

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 \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"

unfolding 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]"

(*>*)

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. 

\noindent

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 Isabelle/HOL and other HOL theorem provers,

since they 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.

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

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