--- a/Paper/Paper.thy Mon Apr 01 21:38:53 2013 +0100
+++ b/Paper/Paper.thy Fri Apr 05 09:18:17 2013 +0100
@@ -300,9 +300,16 @@
%represented as inductively defined predicates too.
\noindent
-The motivation of this paper is to bring the ability to reason
-about results from computability theory, for example decidability of the halting problem,
-to the theorem prover Isabelle/HOL. Norrish formalised computability
+One concete model of computation are Turing machines. We use them
+in the theorem prover Isabelle/HOL for mechanising results from
+computability theory, for example the undecidability of the halting problem.
+Reasoning about decidability is not as straightforward as one might think
+in Isabelle/HOL and other HOL theorem provers,
+since they are based on classical logic where the law of excluded
+middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
+matter whether the predicate @{text P} is constructed by computable means.
+
+Norrish formalised computability
theory in HOL4. He choose the $\lambda$-calculus as the starting point
for his formalisation because of its ``simplicity'' \cite[Page
297]{Norrish11}. Part of his formalisation is a clever infrastructure
--- a/Paper/document/root.tex Mon Apr 01 21:38:53 2013 +0100
+++ b/Paper/document/root.tex Fri Apr 05 09:18:17 2013 +0100
@@ -62,8 +62,9 @@
universal function and obtaining from it a universal Turing machine by
our verified translation from recursive functions to abacus programs
and from abacus programs to Turing machine programs. Hoare-style reasoning techniques allow us
-to reason about Turing machine and abacus programs. Our theory can be
-used to formalise other computability results.
+to reason about concrete Turing machine and abacus programs.
+%Our theory can be
+%used to formalise other computability results.
%We give one example about the computational equivalence of
%single-sided Turing machines.
%{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
Binary file paper.pdf has changed