tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:bd320b5365e2
+:d6f04e3e9894
 abc_lm_s ("set") and*)
 haltP ("stdhalt") and
 tcopy ("copy") and
 tape_of ("\<langle>_\<rangle>") and
 tm_comp ("_ \<oplus> _") and
-DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>")
+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>begin\<^esub>")
+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
 declare [[show_question_marks = false]]
 (* THEOREMS *)
 notation (Rule output)
 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
 "_asm" :: "prop \<Rightarrow> asms" ("_")
 lemma nats2tape:
 shows "<([]::nat list)> = []"
-and "<[n]> = Oc \<up> (n + 1)"
+and "<[n]> = <n>"
-and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
+and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"
-apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+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)
+apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)
 done
 lemmas HR1 =
 Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
 lemmas HR2 =
 Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?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
 (*>*)
 section {* Introduction *}
 %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
+We are not the first who formalised Turing machines: we are aware of
-of the work by Asperti and Ricciotti
+the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They
-\cite{AspertiRicciotti12}. They describe a complete formalisation of
+describe a complete formalisation of Turing machines in the Matita
-Turing machines in the Matita theorem prover, including a universal
+theorem prover, including a universal Turing machine. However, they do
-Turing machine. However, they do \emph{not} formalise the undecidability of the
+\emph{not} formalise the undecidability of the halting problem since
-halting problem since their main focus is complexity, rather than
+their main focus is complexity, rather than computability theory. They
-computability theory. They also report that the informal proofs from which they
+also report that the informal proofs from which they started are not
-started are not ``sufficiently accurate to be directly usable as a
+``sufficiently accurate to be directly usable as a guideline for
-guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
+formalization'' \cite[Page 2]{AspertiRicciotti12}. For our
-our formalisation we follow mainly the proofs from the textbook
+formalisation we follow mainly the proofs from the textbook
 \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 excerise to the reader; also
+the \emph{copy Turing machine} and its correctness proof are left as
-\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
+an excerise to the reader; also \cite{Boolos87} only shows how the
-machines computing unary functions. We had to figure out a way to
+universal Turing machine is constructed for Turing machines computing
-generalise this result to $n$-ary functions. Similarly, when compiling
+unary functions. We had to figure out a way to generalise this result
-recursive functions to abacus machines, the textbook again only shows
+to $n$-ary functions. Similarly, when compiling recursive functions to
-how it can be done for 2- and 3-ary functions, but in the
+abacus machines, the textbook again only shows how it can be done for
-formalisation we need arbitrary functions. But the general ideas for
+2- and 3-ary functions, but in the formalisation we need arbitrary
-how to do this are clear enough in \cite{Boolos87}.
+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.
 \noindent
 In this definition the function @{term nth_of} returns the @{text n}th element
 from a list, provided it exists (@{term Some}-case), or if it does not, it
 returns the default action @{term Nop} and the default state @{text 0}
-(@{term None}-case). We often need to restrict Turing machine programs
+(@{term None}-case). We often have to restrict Turing machine programs
 to be well-formed: a program @{term p} is \emph{well-formed} if it
 satisfies the following three properties:
 \begin{center}
 @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
 \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);
 \end{scope}
 \end{tikzpicture}\\[-8mm]\mbox{}
 \end{center}
 \caption{The three components of the \emph{copy Turing machine} (above). If started
-(below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at
+(below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at
 the end of the right tape; the second then ``moves'' all @{term Oc}s except the
 first from the beginning of the tape to the end; the third ``refills'' the original
-block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
+block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}
 \label{copy}
 \end{figure}
 We often need to restrict tapes to be in \emph{standard form}, which means
 the left list of the tape is either empty or only contains @{text "Bk"}s, and
 the right list contains some ``clusters'' of @{text "Oc"}s separted by single
-blanks. To make this formal we define the following function
+blanks. To make this formal we define the following overloaded function
 \begin{center}
-\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+@{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\
+@{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\
+\end{tabular}\hspace{6mm}
+\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\
 @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\
 @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
 \end{tabular}
 \end{center}
 and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
 leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
 is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
 Before we can prove the undecidability of the halting problem for our
-Turing machines, we need to analyse two concrete Turing machine
+Turing machines, we have to analyse two concrete Turing machine
 programs and establish that they are correct---that means they are
 ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
-out in the informal literature, for example \cite{Boolos87}.  One program
+out in the informal literature, for example \cite{Boolos87}.  The first program
 we need to prove correct is the @{term dither} program shown in \eqref{dither}
 and the other program is @{term "tcopy"} defined as
 \begin{equation}
 \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
 \end{tabular}}\label{tcopy}
 \end{equation}
 \noindent
-whose three components are given in Figure~\ref{copy}. To the prove
+whose three components are given in Figure~\ref{copy}. We introduce
-the correctness of Turing machine programs, we introduce the
+the notion of total correctness defined in terms of
-notion of total correctness defined in terms of
+\emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
-\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
+very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
-to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.
+The Hoare-triples implement the idea that a program @{term p}
-They implement the
+started in state @{term "1::nat"} with a tape satisfying @{term P}
-idea that a program @{term p} started in state @{term "1::nat"} with
+will after some @{text n} steps halt (have transitioned into the
-a tape satisfying @{term P} will after some @{text n} steps halt (have
+halting state) with a tape satisfying @{term Q}. We also have
-transitioned into the halting state) with a tape satisfying @{term
+\emph{Hoare-pairs} of the form @{term "{P} p \<up>"} implementing the
-Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
+case that a program @{term p} started with a tape satisfying @{term
-implementing the case that a program @{term p} started with a tape
+P} will loop (never transition into the halting state). Both notion
-satisfying @{term P} will loop (never transition into the halting
+are formally defined as
-state). Both notion are formally defined as
 \begin{center}
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
 \begin{tabular}[t]{@ {}l@ {}}
 \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
 \noindent
 The first is by a simple calculation. The second is by induction on the
 number of steps we can perform starting from the input tape.
 The program @{term tcopy} defined in \eqref{tcopy} has 15 states;
-its purpose is to produce the standard tape @{term "(DUMMY, <[n,
+its purpose is to produce the standard tape @{term "(DUMMY, <(n,
-n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is
+n::nat)>)"} when started with @{term "(DUMMY, <(n::nat)>)"}, that is
 making a copy of a value on the tape.  Reasoning about this program
 is substantially harder than about @{term dither}. To ease the
-burden, we prove the following two Hoare-rules for sequentially
+burden, we derive the following two Hoare-rules for sequentially
 composed programs.
 \begin{center}
 \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
 $\inferrule*[Right=@{thm (prem 3) HR1}]
 terminates generating a tape for which the second program loops.
 The side-condition about @{thm (prem 3) HR2} is needed in both rules
 in order to ensure that the redirection of the halting and initial
 state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
 The Hoare-rules above allow us to prove the correctness of @{term tcopy}
-by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
+by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"}
 and @{term "tcopy_end"} in isolation. We will show the details for
-the program @{term "tcopy_begin"}. We found the following invariants for each
+the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"}
-state:
+shown in Figure~\ref{invbegin},
+we define the following invariant for @{term "tcopy_begin"}.
-\begin{center}
-@{thm inv_begin0.simps}\\
+\begin{figure}
-@{thm inv_begin1.simps}\\
+\begin{center}
-@{thm inv_begin2.simps}\\
+\begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
-@{thm inv_begin3.simps}\\
+@{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
-@{thm inv_begin4.simps}
+&             & @{thm (rhs) inv_begin02} \\
-\end{center}
+@{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
+@{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
+@{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
+@{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}
+\end{tabular}
+\end{center}
+\caption{The invariants for each state of @{term tcopy_begin}. They depend on
+the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
+\end{figure}
+\begin{center}
+\begin{tabular}{rcl}
+@{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} &
+@{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\
+& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\
+& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\
+& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\
+& & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\
+& & @{text else} @{thm (rhs) inv_begin_print(6)}
+\end{tabular}
+\end{center}
+\noindent
+This definition depends on @{term n}, which represents the number
+of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script)
+to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}.
 measure for the copying TM, which we however omit.
+\begin{center}
+@{thm begin_correct}\\
+@{thm loop_correct}\\
+@{thm end_correct}
+\end{center}
 \begin{center}
 @{thm haltP_def[where lm="ns"]}
 \end{center}

changeset 97	d6f04e3e9894
parent 96	bd320b5365e2
child 98	860f05037c36