
diff -r bd320b5365e2 -r d6f04e3e9894 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Jan 29 16:37:38 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 02:26:56 2013 +0000
@@ -35,7 +35,41 @@
   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]]
 
@@ -73,12 +107,15 @@
 
 lemma nats2tape:
   shows "<([]::nat list)> = []"
-  and "<[n]> = Oc \<up> (n + 1)"
-  and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
-apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
+  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)
-done
+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"]
@@ -86,6 +123,16 @@
 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 *}
@@ -179,26 +226,27 @@
 %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
+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
 \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 
-\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}. 
+the \emph{copy Turing machine} and its correctness proof are left as
+an excerise to the reader; 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
@@ -443,7 +491,7 @@
   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:
 
@@ -638,10 +686,10 @@
   \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}
 
@@ -649,10 +697,14 @@
   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)}
@@ -666,10 +718,10 @@
   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
 
@@ -680,19 +732,18 @@
   \end{equation}
 
   \noindent
-  whose three components are given in Figure~\ref{copy}. To the prove
-  the correctness of Turing machine programs, we introduce the
-  notion of total correctness defined in terms of
-  \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
-  to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.  
-  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}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<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
+  whose three components are given in Figure~\ref{copy}. We introduce
+  the notion of total correctness defined in terms of
+  \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
+  very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
+  The Hoare-triples 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}. We also have
+  \emph{Hoare-pairs} of the form @{term "{P} p \<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}
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
@@ -796,11 +847,11 @@
   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,
-  n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is
+  its purpose is to produce the standard tape @{term "(DUMMY, <(n,
+  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}
@@ -825,23 +876,56 @@
   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 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"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"} 
+  shown in Figure~\ref{invbegin},
+  we define the following invariant for @{term "tcopy_begin"}.
 
-  The Hoare-rules above allow us to prove the correctness of @{term tcopy}
-  by considering the correctness of @{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
-  state:
+  \begin{figure}
+  \begin{center}
+  \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
+  @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+                                &             & @{thm (rhs) inv_begin02} \\
+  @{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}
-  @{thm inv_begin0.simps}\\
-  @{thm inv_begin1.simps}\\
-  @{thm inv_begin2.simps}\\
-  @{thm inv_begin3.simps}\\
-  @{thm inv_begin4.simps}
+  \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}
 
 
-  measure for the copying TM, which we however omit.
 
   \begin{center}
   @{thm haltP_def[where lm="ns"]}




