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

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

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

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

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

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

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

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

    91   rec_calc_rel ("eval") and 

    91   rec_calc_rel ("eval") and 

    93 

    94 

    94  

    95  

    95 lemma inv_begin_print:

    96 lemma inv_begin_print:

    96   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

    97   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

    97         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

    98         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

   170 by(simp add: adjust.simps)

   171 by(simp add: adjust.simps)

   171 

   172 

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

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

   173   where

   174   where

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

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

   175 (*>*)

   261 (*>*)

   176 

   262 

   177 section {* Introduction *}

   263 section {* Introduction *}

   178 

   264 

   179 

   265 

   231 \noindent

   317 \noindent

   232 In this paper we take on this daunting prospect and provide a

   318 In this paper we take on this daunting prospect and provide a

   233 formalisation of Turing machines, as well as abacus machines (a kind

   319 formalisation of Turing machines, as well as abacus machines (a kind

   234 of register machines) and recursive functions. To see the difficulties

   320 of register machines) and recursive functions. To see the difficulties

   235 involved with this work, one has to understand that Turing machine

   321 involved with this work, one has to understand that Turing machine

   245 

   332 

   246 %To see the difficulties

   333 %To see the difficulties

   247 %involved with this work, one has to understand that interactive

   334 %involved with this work, one has to understand that interactive

   248 %theorem provers, like Isabelle/HOL, are at their best when the

   335 %theorem provers, like Isabelle/HOL, are at their best when the

   249 %data-structures at hand are ``structurally'' defined, like lists,

   336 %data-structures at hand are ``structurally'' defined, like lists,

   604   where @{term "read r"} returns the head of the list @{text r}, or if

   691   where @{term "read r"} returns the head of the list @{text r}, or if

   605   @{text r} is empty it returns @{term Bk}.  It is impossible in

   692   @{text r} is empty it returns @{term Bk}.  It is impossible in

   606   Isabelle/HOL to lift the @{term step}-function in order to realise a

   693   Isabelle/HOL to lift the @{term step}-function in order to realise a

   607   general evaluation function for Turing machines programs. The reason

   694   general evaluation function for Turing machines programs. The reason

   608   is that functions in HOL-based provers need to be terminating, and

   695   is that functions in HOL-based provers need to be terminating, and

   610   recursive evaluation function that performs exactly @{text n} steps:

   699   recursive evaluation function that performs exactly @{text n} steps:

   611 

   700 

   612   \begin{center}

   701   \begin{center}

   613   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   702   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   614   @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\

   703   @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\

  1218 

  1307 

  1219   \noindent

  1308   \noindent

  1220   This gives us a list of natural numbers specifying how many states

  1309   This gives us a list of natural numbers specifying how many states

  1221   are needed to translate each abacus instruction. This information

  1310   are needed to translate each abacus instruction. This information

  1222   is needed in order to calculate the state where the Turing machine program

  1311   is needed in order to calculate the state where the Turing machine program

  1227   The @{text Goto}

  1322   The @{text Goto}

  1228   instruction is easiest to translate requiring only one state, namely

  1323   instruction is easiest to translate requiring only one state, namely

  1229   the Turing machine program:

  1324   the Turing machine program:

  1230 

  1325 

  1231   \begin{center}

  1326   \begin{center}

  1243 

  1338 

  1244   \begin{center}

  1339   \begin{center}

  1245   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

  1340   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

  1246   @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\

  1341   @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\

  1247   @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\

  1342   @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\

  1249   \end{tabular}

  1344   \end{tabular}

  1250   \end{center}

  1345   \end{center}

  1251 

  1346 

  1252   \noindent

  1347   \noindent

  1253   Then we need to increase the ``number'' on the tape by one,

  1348   Then we need to increase the ``number'' on the tape by one,