--- a/IsaMakefile Wed Dec 26 14:52:14 2012 +0000
+++ b/IsaMakefile Wed Dec 26 19:03:06 2012 +0000
@@ -14,7 +14,7 @@
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d pdf ## -D generated
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -D generated
## utm
@@ -22,18 +22,14 @@
utm: $(OUT)/utm
$(OUT)/utm: *.thy
- @$(USEDIR) -b HOL UTM
+ @$(USEDIR) -f ROOT.ML -b HOL UTM
-session: ROOT.ML \
+paper: ROOT.ML \
document/root* \
*.thy
- @$(USEDIR) -D generated -f ROOT.ML UTM .
-
-paper: utm
- rm -f generated/*.aux # otherwise latex will fall over
- cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
-# cd generated ; bibtex root
-# cd generated ; $(ISABELLE_TOOL) latex -o pdf root.tex
+ rm -rf generated # otherwise latex will fall over
+ @$(USEDIR) -f ROOT1.ML UTM .
+ $(ISABELLE_TOOL) document -o pdf generated
cp generated/root.pdf paper.pdf
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ROOT1.ML Wed Dec 26 19:03:06 2012 +0000
@@ -0,0 +1,24 @@
+(*
+ turing_basic.thy : The basic definitions of Turing Machine.
+ uncomputable.thy : The existence of Turing uncomputable functions.
+ abacus.thy : The basic definitions of Abacus machine (An intermediate langauge underneath recursive functions) and
+ the compilation of Abacus machines into Turing Machines.
+ rec_def.thy: The basic definitions of Recursive Functions.
+ recursive.thy : The compilation of Recursive Functions into
+ Abacus machines.
+ UF.thy : The construction of Universal Function, named "rec_F" and the proof of its correctness.
+ UTM.thy: Obtaining Uinversal Turing Machine by scarfolding the Turing Machine compiled from "rec_F" with some
+ initialization and termination processing Turing Machines.
+*)
+
+no_document
+use_thys ["turing_basic",
+ "uncomputable",
+ "abacus",
+ "rec_def",
+ "recursive",
+ "UF",
+ "UTM"];
+
+
+use_thys ["Paper"]
--- a/document/root.tex Wed Dec 26 14:52:14 2012 +0000
+++ b/document/root.tex Wed Dec 26 19:03:06 2012 +0000
@@ -34,28 +34,29 @@
\begin{document}
-\title{A Formalised Theorey about Turing Machines in Isablle/HOL}
+\title{A Formalised Theory of Turing Machines in Isabelle/HOL}
-\author{\IEEEauthorblockN{Authors Name/s per 1st Affiliation (Author)}
-\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
-line 2: name of organization, acronyms acceptable\\
-line 3: City, Country\\
-line 4: Email: name@xyz.com}
+\author{
+\IEEEauthorblockN{Xu Jian, Xingyuan Zhang}
+\IEEEauthorblockA{PLA University of Science and Technology Nanjing, China}
\and
-\IEEEauthorblockN{Authors Name/s per 2nd Affiliation (Author)}
-\IEEEauthorblockA{line 1 (of Affiliation): dept. name of organization\\
-line 2: name of organization, acronyms acceptable\\
-line 3: City, Country\\
-line 4: Email: name@xyz.com}
+\IEEEauthorblockN{Christian Urban}
+\IEEEauthorblockA{King's College London, UK}
}
\maketitle
\begin{abstract}
-
-The abstract goes here. DO NOT USE SPECIAL CHARACTERS, SYMBOLS, OR MATH IN YOUR TITLE OR ABSTRACT.
+Isabelle/HOL is an interactive theorem prover based on classical
+logic. While classical reasoning allow users to take convenient
+shortcuts in some proofs, it precludes \emph{direct} reasoning about
+decidability: every boolean predicate is either true or false
+because of the law of excluded middle. The only way to reason
+about decidability in a classical theorem prover, like Isabelle/HOL,
+is to formalise a concrete model for computation. In this paper
+we formalise Turing machines and relate them to register machines.
\end{abstract}
@@ -73,16 +74,6 @@
\parindent 0pt\parskip 0.5ex
-\section{Introduction}
-
-text {*
-
-
-*}
-
-
-\noindent
-{\bf Contributions:}
% generated text of all theories
Binary file paper.pdf has changed