# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1356548586 0
# Node ID 26b17f2d583e18be42f0dff74e093d9ffff24f3f
# Parent  4b9aa15ff713b06e3ecab56048eafc8c02cb7fda
updated

diff -r 4b9aa15ff713 -r 26b17f2d583e IsaMakefile
--- 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  
 
 
diff -r 4b9aa15ff713 -r 26b17f2d583e ROOT1.ML
--- /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"]
diff -r 4b9aa15ff713 -r 26b17f2d583e document/root.tex
--- 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
diff -r 4b9aa15ff713 -r 26b17f2d583e paper.pdf
Binary file paper.pdf has changed