--- a/Paper/Paper.thy Wed Mar 27 09:47:02 2013 +0000
+++ b/Paper/Paper.thy Wed Mar 27 13:16:37 2013 +0000
@@ -88,7 +88,7 @@
Pr ("Pr\<^isup>_") and
Cn ("Cn\<^isup>_") and
Mn ("Mn\<^isup>_") and
- rec_calc_rel ("eval") and
+ rec_exec ("eval") and
tm_of_rec ("translate") and
listsum ("\<Sigma>")
@@ -103,9 +103,10 @@
apply(case_tac [!] tp)
by (auto)
+
lemma inv1:
- shows "0 < n \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
-unfolding assert_imp_def
+ 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)
@@ -872,13 +873,13 @@
\noindent
whose three components are given in Figure~\ref{copy}. For our
correctness proofs, we introduce the notion of total correctness
- defined in terms of \emph{Hoare-triples}, written @{term "{P} p
+ defined in terms of \emph{Hoare-triples}, written @{term "{P} (p::tprog0)
{Q}"}. They implement the idea that a program @{term
p} started in state @{term "1::nat"} with a tape satisfying @{term
P} will after some @{text n} steps halt (have transitioned into the
halting state) with a tape satisfying @{term Q}. This idea is very
similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We
- also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
+ also have \emph{Hoare-pairs} of the form @{term "{P} (p::tprog0) \<up>"}
implementing the case that a program @{term p} started with a tape
satisfying @{term P} will loop (never transition into the halting
state). Both notion are formally defined as
@@ -911,7 +912,7 @@
\noindent
where
- @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
+ @{term "Turing_Hoare.assert_imp P' P"} stands for the fact that for all tapes @{term "tp"},
@{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
Like Asperti and Ricciotti with their notion of realisability, we
@@ -1122,8 +1123,8 @@
where we assume @{text "0 < n"} (similar reasoning is needed for
the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
the halting state of @{term tcopy_begin} implies the invariant of
- the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
- n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
+ the starting state of @{term tcopy_loop}, that is @{term "Turing_Hoare.assert_imp (inv_begin0 n)
+ (inv_loop1 n)"} holds, and also @{term "inv_loop0 n = inv_end1
n"}, we can derive the following Hoare-triple for the correctness
of @{term tcopy}:
@@ -1406,9 +1407,9 @@
& @{text "|"} & @{term "id n m"} & (projection)\\
\end{tabular} &
\begin{tabular}{cl@ {\hspace{4mm}}l}
- @{text "|"} & @{term "Cn n r rs"} & (composition)\\
- @{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
- @{text "|"} & @{term "Mn n r"} & (minimisation)\\
+ @{text "|"} & @{term "Cn n f fs"} & (composition)\\
+ @{text "|"} & @{term "Pr n f\<^isub>1 f\<^isub>2"} & (primitive recursion)\\
+ @{text "|"} & @{term "Mn n f"} & (minimisation)\\
\end{tabular}
\end{tabular}
\end{center}
@@ -1416,29 +1417,32 @@
\noindent
where @{text n} indicates the function expects @{term n} arguments
(in \cite{Boolos87} both @{text z} and @{term s} expect one
- argument), and @{text rs} stands for a list of recursive
+ argument), and @{text fs} stands for a list of recursive
functions. Since we know in each case the arity, say @{term l}, we
- can define an inductive evaluation relation that relates a recursive
- function @{text r} and a list @{term ns} of natural numbers of
- length @{text l}, to what the result of the recursive function is,
- say @{text n}. We omit the definition of @{term "rec_calc_rel r ns
- n"}. Because of space reasons, we also omit the definition of
+ can define an evaluation function, called @{term rec_exec}, that takes a recursive
+ function @{text f} and a list @{term ns} of natural numbers of
+ length @{text l} as arguments. Since this evaluation function uses
+ the minimisation operator
+ from HOL, this function might not terminate always. As a result we also
+ need to inductively characterise when @{term rec_exec} terminates.
+ We omit the definitions for
+ @{term "rec_exec f ns"} and @{term "terminate f ns"}. Because of
+ space reasons, we also omit the definition of
translating recursive functions into abacus programs. We can prove,
however, the following theorem about the translation: If @{thm (prem
- 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and
- r="n"]} holds for the recursive function @{text r}, then the
+ 1) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]}
+ holds for the recursive function @{text f} and arguments @{term ns}, then the
following Hoare-triple holds
\begin{center}
- @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]}
+ @{thm (concl) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]}
\end{center}
\noindent
- for the translated Turing machine @{term "translate r"}. This
- means that if the recursive function @{text r} with arguments @{text ns} evaluates
- to @{text n}, then the translated Turing machine if started
+ for the Turing machine generated by @{term "translate f"}. This
+ means the translated Turing machine if started
with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate
- with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
+ with the standard tape @{term "(Bk \<up> k, <(rec_exec f ns)::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}.
Having recursive functions under our belt, we can construct a universal
function, written @{text UF}. This universal function acts like an interpreter for Turing machines.
@@ -1560,12 +1564,13 @@
If started with standard tape @{term "([], [Oc])"}, it halts with the
non-standard tape @{term "([Oc], [])"} according to the definition in Chapter 3---so no
result is calculated; but with the standard tape @{term "([], [Oc])"} according to the
- definition in Chapter 8. We solve this inconsitency in our formalisation by
+ definition in Chapter 8.
+ We solve this inconsistency in our formalisation by
setting up our definitions so that the @{text counter_example} Turing machine does not
produce any result by looping forever fetching @{term Nop}s in state @{text 0}.
- This solution is different from the definition in Chapter 3, but also
- different from the one in Chapter 8, where the instruction from state @{text 1} is
- fetched.
+ This solution implements essentially the definition in Chapter 3; it
+ differs from the definition in Chapter 8, where perplexingly the instruction
+ from state @{text 1} is fetched.
*}
(*
@@ -1676,7 +1681,7 @@
functions and abacus machines, we agree, is not a project
one wants to undertake too many times (our formalisation of abacus
machines and their correct translation is approximately 4600 loc;
- recursive functions 5000 loc and the universal Turing machine 10000 loc).
+ recursive functions 2800 loc and the universal Turing machine 10000 loc).
Our work is also very much inspired by the formalisation of Turing
machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the