tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:d8e6f0798e23
+:49dcc0b9b0b3
 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
+rec_exec ("eval") and
 tm_of_rec ("translate") and
 listsum ("\<Sigma>")
 lemma inv_begin_print:
 "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"
+shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"
-unfolding assert_imp_def
+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
 \end{equation}
 \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
 \begin{center}
 @{thm[mode=Rule] Hoare_consequence}
 \end{equation}
 \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
 have set up our Hoare-rules so that we can deal explicitly
 with total correctness and non-termination, rather than have
 \noindent
 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
+the starting state of @{term tcopy_loop}, that is @{term "Turing_Hoare.assert_imp (inv_begin0 n)
-n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
+(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}:
 \begin{center}
 @{thm tcopy_correct}
 @{term r} & @{text "::="} & @{term z} & (zero-function)\\
 & @{text "|"}   & @{term s} & (successor-function)\\
 & @{text "|"}   & @{term "id n m"} & (projection)\\
 \end{tabular} &
 \begin{tabular}{cl@ {\hspace{4mm}}l}
-@{text "|"} & @{term "Cn n r rs"} & (composition)\\
+@{text "|"} & @{term "Cn n f fs"} & (composition)\\
-@{text "|"} & @{term "Pr n r\<^isub>1 r\<^isub>2"} & (primitive recursion)\\
+@{text "|"} & @{term "Pr n f\<^isub>1 f\<^isub>2"} & (primitive recursion)\\
-@{text "|"} & @{term "Mn n r"} & (minimisation)\\
+@{text "|"} & @{term "Mn n f"} & (minimisation)\\
 \end{tabular}
 \end{tabular}
 \end{center}
 \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
+can define an evaluation function, called @{term rec_exec}, that takes a recursive
-function @{text r} and a list @{term ns} of natural numbers of
+function @{text f} and a list @{term ns} of natural numbers of
-length @{text l}, to what the result of the recursive function is,
+length @{text l} as arguments. Since this evaluation function uses
-say @{text n}. We omit the definition of @{term "rec_calc_rel r ns
+the minimisation operator
-n"}. Because of space reasons, we also omit the definition of
+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
+1) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]}
-r="n"]} holds for the recursive function @{text r}, then the
+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
+for the Turing machine generated by @{term "translate f"}. This
-means that if the recursive function @{text r} with arguments @{text ns} evaluates
+means the translated Turing machine if started
-to @{text n}, then 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.
 It takes two arguments: one is the code of the Turing machine to be interpreted and the
 other is the ``packed version'' of the arguments of the Turing machine.
 \noindent
 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
+This solution implements essentially the definition in Chapter 3; it
-different from the one in Chapter 8, where the instruction from state @{text 1} is
+differs from the definition in Chapter 8, where perplexingly the instruction
-fetched.
+from state @{text 1} is fetched.
 *}
 (*
 section {* XYZ *}
 as we estimated when reading the paper by Norrish \cite{Norrish11}. The work
 involved with constructing a universal Turing machine via recursive
 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
 Matita theorem prover. It turns out that their notion of
 realisability and our Hoare-triples are very similar, however we

changeset 230	49dcc0b9b0b3
parent 218	bfa2a8145f79
child 231	b66578c08490