--- a/Paper/Paper.thy Fri Jan 25 15:57:58 2013 +0100
+++ b/Paper/Paper.thy Fri Jan 25 21:15:09 2013 +0000
@@ -27,6 +27,7 @@
tcopy_end ("copy\<^bsub>end\<^esub>") and
step0 ("step") and
steps0 ("steps") and
+ exponent ("_\<^bsup>_\<^esup>") and
(* abc_lm_v ("lookup") and
abc_lm_s ("set") and*)
haltP ("stdhalt") and
@@ -247,10 +248,12 @@
constructors, namely @{text Bk} and @{text Oc}. One way to
represent such tapes is to use a pair of lists, written @{term "(l,
r)"}, where @{term l} stands for the tape on the left-hand side of
- the head and @{term r} for the tape on the right-hand side. We have
- the convention that the head, abbreviated @{term hd}, of the
- right-list is the cell on which the head of the Turing machine
- currently scannes. This can be pictured as follows:
+ the head and @{term r} for the tape on the right-hand side. We use
+ the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
+ composed of @{term n} elements of @{term Bk}. We also have the
+ convention that the head, abbreviated @{term hd}, of the right-list
+ is the cell on which the head of the Turing machine currently
+ scannes. This can be pictured as follows:
%
\begin{center}
\begin{tikzpicture}
@@ -304,7 +307,7 @@
We slightly deviate
from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
will become important when we formalise halting computations and also universal Turing
- machines. Given a tape and an action, we can define the
+ machines. Given a tape and an action, we can define the
following tape updating function:
\begin{center}
@@ -361,7 +364,7 @@
%cannot be used as it does not preserve types.} This renaming can be
%quite cumbersome to reason about.
We follow the choice made in \cite{AspertiRicciotti12}
- representing a state by a natural number and the states in a Turing
+ by representing a state with a natural number and the states in a Turing
machine program by the initial segment of natural numbers starting from @{text 0}.
In doing so we can compose two Turing machine programs by
shifting the states of one by an appropriate amount to a higher
@@ -371,7 +374,7 @@
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
machine is then a list of such pairs. Using as an example the following Turing machine
program, which consists of four instructions
-
+ %
\begin{equation}
\begin{tikzpicture}
\node [anchor=base] at (0,0) {@{thm dither_def}};
@@ -385,7 +388,7 @@
\end{tikzpicture}
\label{dither}
\end{equation}
-
+ %
\noindent
the reader can see we have organised our Turing machine programs so
that segments of two belong to a state. The first component of such a
@@ -401,8 +404,8 @@
\cite{AspertiRicciotti12}, we have chosen a very concrete
representation for programs, because when constructing a universal
Turing machine, we need to define a coding function for programs.
- This can be easily done for our programs-as-lists, but is more
- difficult for the functions used by Asperti and Ricciotti.
+ This can be directly done for our programs-as-lists, but is
+ slightly more difficult for the functions used by Asperti and Ricciotti.
Given a program @{term p}, a state
and the cell being read by the head, we need to fetch
@@ -525,9 +528,21 @@
\caption{Copy machine}\label{copy}
\end{figure}
- {\it
- As in \cite{Boolos87} we often need to restrict tapes to be in standard
- form.}
+ 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 and can be followed by some blanks. To make this formal we define the
+ following function
+
+ \begin{center}
+ foo
+ \end{center}
+
+ \noindent
+ A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+ @{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
+ leftmost @{term "Oc"} on the tape.
+
Before we can prove the undecidability of the halting problem for our
Turing machines, we need to analyse two concrete Turing machine
@@ -549,7 +564,7 @@
notion of total correctness defined in terms of
\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
idea that a program @{term p} started in state @{term "1::nat"} with
- a tape satisfying @{term P} will after @{text n} steps halt (have
+ 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>"}
realising the case that a program @{term p} started with a tape
@@ -577,7 +592,7 @@
\noindent
We have set up our Hoare-style reasoning so that we can deal explicitly
- with looping and total correctness, rather than have notions for partial
+ with total correctness and non-terminantion, rather than have notions for partial
correctness and termination. Although the latter would allow us to reason
more uniformly (only using Hoare-triples), we prefer our definitions because
we can derive simple Hoare-rules for sequentially composed Turing programs.
@@ -585,8 +600,9 @@
for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}.
\begin{center}
- \begin{tabular}{lcl}
- \multicolumn{1}{c}{start tape}\\
+ \begin{tabular}{l@ {\hspace{3mm}}lcl}
+ & \multicolumn{1}{c}{start tape}\\[1mm]
+ \raisebox{2.5mm}{halting case:} &
\begin{tikzpicture}
\draw[very thick] (-2,0) -- ( 0.75,0);
\draw[very thick] (-2,0.5) -- ( 0.75,0.5);
@@ -615,7 +631,8 @@
\node [anchor=base] at (-1.7,0.2) {\ldots};
\end{tikzpicture}\\
- \begin{tikzpicture}
+ \raisebox{2.5mm}{non-halting case:} &
+ \begin{tikzpicture}
\draw[very thick] (-2,0) -- ( 0.25,0);
\draw[very thick] (-2,0.5) -- ( 0.25,0.5);
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
--- a/thys/uncomputable.thy Fri Jan 25 15:57:58 2013 +0100
+++ b/thys/uncomputable.thy Fri Jan 25 21:15:09 2013 +0000
@@ -64,24 +64,23 @@
inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>
- (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
-| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
+ "inv_init0 n (l, r) = ((n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc])) \<or>
+ (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc])))"
+| "inv_init1 n (l, r) = ((l, r) = ([], Oc \<up> n))"
+| "inv_init2 n (l, r) = (\<exists> i j. i > 0 \<and> i + j = n \<and> (l, r) = (Oc \<up> i, Oc \<up> j))"
+| "inv_init3 n (l, r) = (n > 0 \<and> (l, tl r) = (Bk # Oc \<up> n, []))"
+| "inv_init4 n (l, r) = (n > 0 \<and> ((l, r) = (Oc \<up> n, [Bk, Oc]) \<or> (l, r) = (Oc \<up> (n - 1), [Oc, Bk, Oc])))"
fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
- "inv_init x (s, l, r) =
- (if s = 0 then inv_init0 x (l, r)
- else if s = 1 then inv_init1 x (l, r)
- else if s = 2 then inv_init2 x (l, r)
- else if s = 3 then inv_init3 x (l, r)
- else if s = 4 then inv_init4 x (l, r)
+ "inv_init n (s, l, r) =
+ (if s = 0 then inv_init0 n (l, r) else
+ if s = 1 then inv_init1 n (l, r) else
+ if s = 2 then inv_init2 n (l, r) else
+ if s = 3 then inv_init3 n (l, r) else
+ if s = 4 then inv_init4 n (l, r)
else False)"
-declare inv_init.simps[simp del]
lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
@@ -109,20 +108,19 @@
fun init_state :: "config \<Rightarrow> nat"
where
- "init_state (s, l, r) = (if s = 0 then 0
- else 5 - s)"
+ "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
fun init_step :: "config \<Rightarrow> nat"
where
- "init_step (s, l, r) = (if s = 2 then length r
- else if s = 3 then if r = [] \<or> r = [Bk] then Suc 0 else 0
- else if s = 4 then length l
- else 0)"
+ "init_step (s, l, r) =
+ (if s = 2 then length r else
+ if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
+ if s = 4 then length l
+ else 0)"
fun init_measure :: "config \<Rightarrow> nat \<times> nat"
where
- "init_measure c =
- (init_state c, init_step c)"
+ "init_measure c = (init_state c, init_step c)"
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
@@ -131,11 +129,11 @@
definition init_LE :: "(config \<times> config) set"
where
- "init_LE \<equiv> (inv_image lex_pair init_measure)"
+ "init_LE \<equiv> (inv_image lex_pair init_measure)"
lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
-apply(case_tac r, auto, case_tac a, auto)
-done
+by (case_tac r, auto, case_tac a, auto)
+
lemma wf_init_le: "wf init_LE"
by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
@@ -164,11 +162,10 @@
ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) (Suc n),
steps (Suc 0, [], Oc \<up> x) (tcopy_init, 0) n) \<in> init_LE"
using a
- proof(simp)
+ proof(simp del: inv_init.simps)
assume "inv_init x (s, l, r)" "0 < s"
thus "(step (s, l, r) (tcopy_init, 0), s, l, r) \<in> init_LE"
- apply(auto simp: inv_init.simps init_LE_def lex_pair_def step.simps tcopy_init_def numeral
- split: if_splits)
+ apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_init_def numeral split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
@@ -199,48 +196,31 @@
(* tcopy_loop *)
-fun inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop1_loop x (l, r) =
- (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
-
-fun inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop1_exit x (l, r) =
- (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
-fun inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
-
-fun inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop2 x (l, r) =
- (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
-
-fun inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop3 x (l, r) =
- (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
-
-fun inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop4 x (l, r) =
- (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+fun
+ inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop1_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop1_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop4 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop5_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+ inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
- "inv_loop5_loop x (l, r) =
- (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
-
-fun inv_loop5_exit :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
-
-fun inv_loop5 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or>
- inv_loop5_exit x (l, r))"
+ "inv_loop0 x (l, r) = (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
+| "inv_loop1_loop x (l, r) = (\<exists> i j. i + j + 1 = x \<and> l = Oc\<up>i \<and> r = Oc # Oc # Bk\<up>j @ Oc\<up>j \<and> j > 0)"
+| "inv_loop1_exit x (l, r) = (l = [] \<and> r = Bk # Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0)"
+| "inv_loop1 x (l, r) = (inv_loop1_loop x (l, r) \<or> inv_loop1_exit x (l, r))"
+| "inv_loop2 x (l, r) = (\<exists> i j any. i + j = x \<and> x > 0 \<and> i > 0 \<and> j > 0 \<and> l = Oc\<up>i \<and> r = any#Bk\<up>j@Oc\<up>j)"
+| "inv_loop3 x (l, r) =
+ (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = Suc j \<and> l = Bk\<up>k@Oc\<up>i \<and> r = Bk\<up>t@Oc\<up>j)"
+| "inv_loop4 x (l, r) =
+ (\<exists> i j k t. i + j = x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> l = Oc\<up>k @ Bk\<up>(Suc j)@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_loop x (l, r) =
+ (\<exists> i j k t. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> k + t = j \<and> t > 0 \<and> l = Oc\<up>k@Bk\<up>j@Oc\<up>i \<and> r = Oc\<up>t)"
+| "inv_loop5_exit x (l, r) = (\<exists> i j. i + j = Suc x \<and> i > 0 \<and> j > 0 \<and> l = Bk\<up>(j - 1)@Oc\<up>i \<and> r = Bk # Oc\<up>j)"
+| "inv_loop5 x (l, r) = (inv_loop5_loop x (l, r) \<or> inv_loop5_exit x (l, r))"
fun inv_loop6_loop :: "nat \<Rightarrow> tape \<Rightarrow> bool"
where
@@ -256,11 +236,6 @@
where
"inv_loop6 x (l, r) = (inv_loop6_loop x (l, r) \<or> inv_loop6_exit x (l, r))"
-fun inv_loop0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
- where
- "inv_loop0 x (l, r) =
- (l = [Bk] \<and> r = Oc # Bk\<up>x @ Oc\<up>x \<and> x > 0 )"
-
fun inv_loop :: "nat \<Rightarrow> config \<Rightarrow> bool"
where
"inv_loop x (s, l, r) =
@@ -277,21 +252,20 @@
inv_loop2.simps[simp del] inv_loop3.simps[simp del]
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
inv_loop6.simps[simp del]
+
lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
-apply(case_tac t, auto)
-done
-
+by (case_tac t, auto)
lemma [simp]: "inv_loop1 x (b, []) = False"
by(simp add: inv_loop1.simps)
lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop2.simps inv_loop3.simps)
-done
+by (auto simp: inv_loop2.simps inv_loop3.simps)
+
lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
-apply(auto simp: inv_loop3.simps)
-done
+by (auto simp: inv_loop3.simps)
+
lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
@@ -1070,10 +1044,10 @@
(* invariants of dither *)
abbreviation
- "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
+ "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
abbreviation
- "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
+ "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
lemma dither_loops_aux:
"(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
@@ -1330,9 +1304,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
- def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+ def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+ def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+ def P3 \<equiv> "\<lambda>(l, r). (\<exists>n. (l, r) = (Bk \<up> n, [Oc, Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1349,12 +1323,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (rule tcopy_correct2)
+ by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (rule H_halt_inv)
+ using assms by (simp) (rule H_halt_inv)
qed (simp)
(* {P3} dither {P3} *)
@@ -1384,9 +1358,9 @@
shows "False"
proof -
(* invariants *)
- def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [] \<and> r = <[code_tcontra]>)"
- def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l = [Bk] \<and> r = <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+ def P1 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([], <[code_tcontra]>)"
+ def P2 \<equiv> "\<lambda>(l::cell list, r::cell list). (l, r) = ([Bk], <[code_tcontra, code_tcontra]>)"
+ def P3 \<equiv> "\<lambda>(l::cell list, r::cell list). (\<exists>n. (l, r) = (Bk \<up> n, [Oc]))"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1403,12 +1377,12 @@
proof (cases rule: Hoare_plus_halt_simple)
case A_halt (* of tcopy *)
show "{P1} tcopy {P2}" unfolding P1_def P2_def
- by (rule tcopy_correct2)
+ by (simp) (rule tcopy_correct2)
next
case B_halt (* of H *)
then show "{P2} H {P3}"
unfolding P2_def P3_def
- using assms by (rule H_unhalt_inv)
+ using assms by (simp) (rule H_unhalt_inv)
qed (simp)
(* {P3} dither loops *)