# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1378216972 -3600
# Node ID a21fb87bb0bdca8a628bd18940ebe7b6e43b3bed
# Parent  7d29c3c09bea70bb8d93b1678c810ca7ee52c9a0
soem changes

diff -r 7d29c3c09bea -r a21fb87bb0bd Literature/fictious_sl_sharing-conf.pdf
Binary file Literature/fictious_sl_sharing-conf.pdf has changed
diff -r 7d29c3c09bea -r a21fb87bb0bd Paper/Paper.thy
--- a/Paper/Paper.thy	Sat Jul 27 08:23:09 2013 +0200
+++ b/Paper/Paper.thy	Tue Sep 03 15:02:52 2013 +0100
@@ -73,23 +73,23 @@
   tape_of ("\<langle>_\<rangle>") and 
   tm_comp ("_ ; _") and 
   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_begin0 ("I\<^sub>0") and
+  inv_begin1 ("I\<^sub>1") and
+  inv_begin2 ("I\<^sub>2") and
+  inv_begin3 ("I\<^sub>3") and
+  inv_begin4 ("I\<^sub>4") and 
   inv_begin ("I\<^bsub>cbegin\<^esub>") and
-  inv_loop1 ("J\<^isub>1") and
-  inv_loop0 ("J\<^isub>0") and
-  inv_end1 ("K\<^isub>1") and
-  inv_end0 ("K\<^isub>0") and
+  inv_loop1 ("J\<^sub>1") and
+  inv_loop0 ("J\<^sub>0") and
+  inv_end1 ("K\<^sub>1") and
+  inv_end0 ("K\<^sub>0") and
   measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
   layout_of ("layout") and
   findnth ("find'_nth") and
-  recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
-  Pr ("Pr\<^isup>_") and
-  Cn ("Cn\<^isup>_") and
-  Mn ("Mn\<^isup>_") and
+  recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and
+  Pr ("Pr\<^sup>_") and
+  Cn ("Cn\<^sup>_") and
+  Mn ("Mn\<^sup>_") and
   rec_exec ("eval") and
   tm_of_rec ("translate") and
   listsum ("\<Sigma>")
@@ -145,10 +145,10 @@
 done 
 
 lemmas HR1 = 
-  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]
 
 lemmas HR2 =
-  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
+  Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]
 
 lemma inv_begin01:
   assumes "n > 1"
@@ -645,7 +645,7 @@
   \end{equation}
   %
   \noindent
-  A \emph{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}, 
+  A \emph{standard tape} is then of the form @{text "(Bk\<^sup>k,\<langle>[n\<^sub>1,...,n\<^sub>m]\<rangle> @ Bk\<^sup>l)"} for some @{text k}, 
   @{text l} 
   and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the 
   leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 
@@ -670,18 +670,18 @@
   0}-state, thus redirecting all references to the ``halting state''
   to the first state after the program @{text p}.  With these two
   functions in place, we can define the \emph{sequential composition}
-  of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} as
+  of two Turing machine programs @{text "p\<^sub>1"} and @{text "p\<^sub>2"} as
 
   \begin{center}
-  @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+  @{thm tm_comp.simps[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2", THEN eq_reflection]}
   \end{center}
 
   \noindent
-  %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+  %This means @{text "p\<^sub>1"} is executed first. Whenever it originally
   %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
-  %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+  %state of @{text "p\<^sub>2"} instead. All the states of @{text "p\<^sub>2"}
   %have been shifted in order to make sure that the states of the composed 
-  %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 
+  %program @{text "p\<^sub>1 \<oplus> p\<^sub>2"} still only ``occupy'' 
   %an initial segment of the natural numbers.
   
   \begin{figure}[t]
@@ -970,7 +970,7 @@
   the first program terminates generating a tape for which the second
   program loops.  The side-conditions about @{thm (prem 3) HR2} are
   needed in order to ensure that the redirection of the halting and
-  initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match
+  initial state in @{term "p\<^sub>1"} and @{term "p\<^sub>2"}, respectively, match
   up correctly.  These Hoare-rules 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"}
@@ -1128,25 +1128,25 @@
   \end{center}
 
   \noindent
-  Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"} 
+  Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^sub>1"}\ldots@{text "P\<^sub>3"} 
   shown on the 
   left, we can derive the following Hoare-pair for @{term tcontra} on the right.
 
   \begin{center}\small
   \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
-  @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+  @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
   \end{tabular}
   &
   \begin{tabular}[b]{@ {}l@ {}}
   \raisebox{-20mm}{$\inferrule*{
-    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
-    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
-    \\ @{term "{P\<^isub>3} dither \<up>"}
+    \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}}
+    {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}}
+    \\ @{term "{P\<^sub>3} dither \<up>"}
    }
-   {@{term "{P\<^isub>1} tcontra \<up>"}}
+   {@{term "{P\<^sub>1} tcontra \<up>"}}
   $}
   \end{tabular}
   \end{tabular}
@@ -1157,25 +1157,25 @@
   with @{term "<(code tcontra)>"} halts.
 
   Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants 
-  @{text "Q\<^isub>1"}\ldots@{text "Q\<^isub>3"}
+  @{text "Q\<^sub>1"}\ldots@{text "Q\<^sub>3"}
   shown on the 
   left, we can derive the Hoare-triple for @{term tcontra} on the right.
 
   \begin{center}\small
   \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
-  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
-  @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
-  @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+  @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
   \end{tabular}
   &
   \begin{tabular}[t]{@ {}l@ {}}
   \raisebox{-20mm}{$\inferrule*{
-    \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
-    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
-    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+    \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}}
+    {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}}
+    \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"}
    }
-   {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+   {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}}
   $}
   \end{tabular}
   \end{tabular}
@@ -1196,8 +1196,8 @@
   \noindent
   Boolos et al \cite{Boolos87} use abacus machines as a stepping stone
   for making it less laborious to write Turing machine
-  programs. Abacus machines operate over a set of registers @{text "R\<^isub>0"},
-  @{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>n"} each being able to hold an arbitrary large natural
+  programs. Abacus machines operate over a set of registers @{text "R\<^sub>0"},
+  @{text "R\<^sub>1"}, \ldots{}, @{text "R\<^sub>n"} each being able to hold an arbitrary large natural
   number.  We use natural numbers to refer to registers; we also use a natural number
   to represent a program counter and to represent jumping ``addresses'', for which we 
   use the letter @{text l}. An abacus 
@@ -1354,7 +1354,7 @@
   \end{tabular} &
   \begin{tabular}{cl@ {\hspace{4mm}}l}
   @{text "|"} & @{term "Cn n f fs"} & (composition)\\
-  @{text "|"} & @{term "Pr n f\<^isub>1 f\<^isub>2"} & (primitive recursion)\\
+  @{text "|"} & @{term "Pr n f\<^sub>1 f\<^sub>2"} & (primitive recursion)\\
   @{text "|"} & @{term "Mn n f"} & (minimisation)\\
   \end{tabular}
   \end{tabular}
diff -r 7d29c3c09bea -r a21fb87bb0bd Paper/document/root.tex
--- a/Paper/document/root.tex	Sat Jul 27 08:23:09 2013 +0200
+++ b/Paper/document/root.tex	Tue Sep 03 15:02:52 2013 +0100
@@ -58,7 +58,7 @@
 %theorem prover is to formalise a concrete model of computation.  
 Following the textbook by Boolos et al, we formalise Turing machines
 and relate them to abacus machines and recursive functions. We ``tie
-the know'' between these three computational models by formalising a
+the knot'' between these three computational models by formalising a
 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
diff -r 7d29c3c09bea -r a21fb87bb0bd paper.pdf
Binary file paper.pdf has changed
diff -r 7d29c3c09bea -r a21fb87bb0bd thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Sat Jul 27 08:23:09 2013 +0200
+++ b/thys2/UF_Rec.thy	Tue Sep 03 15:02:52 2013 +0100
@@ -659,6 +659,6 @@
   "rec_eval rec_uf [m, cf] = UF m cf"
 by (simp add: rec_uf_def)
 
-value "size rec_uf"
+(* value "size rec_uf" *)
 end