--- a/Paper/Paper.thy	Mon Apr 22 10:33:40 2013 +0100
+++ b/Paper/Paper.thy	Wed Apr 24 09:49:00 2013 +0100
@@ -191,75 +191,10 @@
 apply(arith)+
 done
 
-(*
-lemma "run tcopy (1, [], <0::nat>) = (0, [Bk], [Oc, Bk, Oc])"
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral nth_of.simps del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
-apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps)
-apply(simp only: numeral[symmetric])
-apply(simp)
-apply(subst run.simps)
-apply(simp)
+lemma tm_wf_simps:
+  "tm_wf0 p = (2 <=length p \<and> is_even(length p) \<and> (\<forall>(a,s) \<in> set p. s <= (length p) div 2))"
+apply(simp add: tm_wf.simps)
 done
-*)
 
 (*>*)
 
@@ -420,7 +355,7 @@
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed by translating from a (universal) recursive function. 
 The part of mechanising the translation of recursive function to register 
-machines has already been done by Zammit in HOL \cite{Zammit99}, 
+machines has already been done by Zammit in HOL4 \cite{Zammit99}, 
 although his register machines use a slightly different instruction
 set than the one described in \cite{Boolos87}.
 
@@ -506,12 +441,8 @@
   \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
   @{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\
   & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
-  \end{tabular}
-  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
   & $\mid$ & @{term L} & (move left)\\
   & $\mid$ & @{term R} & (move right)\\
-  \end{tabular}
-  \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
   & $\mid$ & @{term Nop} & (do-nothing operation)\\
   \end{tabular}
   \end{center}
@@ -645,7 +576,7 @@
   satisfies the following three properties:
 
   \begin{center}
-  @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
+  @{thm tm_wf_simps[where p="p", THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -903,17 +834,17 @@
   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}
   \begin{tabular}[t]{@ {}l@ {}}
   \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]
-  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
-  \hspace{7mm}if @{term "P (l, r)"} holds then\\
-  \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
-  \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
-  \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\
+  \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
+  \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
   \end{tabular} &
   \begin{tabular}[t]{@ {}l@ {}}
   \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
-  \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ 
-  \hspace{7mm}if @{term "P (l, r)"} holds then\\
-  \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"}
+  \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 
+  \hspace{7mm}if @{term "P tp"} holds then\\
+  \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
   \end{tabular}
   \end{tabular}
   \end{center}
@@ -998,7 +929,7 @@
   \end{center}
 
   \noindent
-  We can prove the following Hoare-statements:
+  We can prove the following two Hoare-statements:
  
   \begin{center}
   \begin{tabular}{l}
@@ -1308,7 +1239,7 @@
   Turing machine programs. Registers and their content are represented by
   standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it
   is impossible to build Turing machine programs out of components 
-  using our @{text "\<oplus>"}-operation shown in the previous section.
+  using our @{text ";"}-operation shown in the previous section.
   To overcome this difficulty, we calculate a \emph{layout} of an
   abacus program as follows
 
@@ -1465,13 +1396,13 @@
   other is the ``packed version'' of the arguments of the Turing machine. 
   We can then consider how this universal function is translated to a 
   Turing machine and from this construct the universal Turing machine, 
-  written @{term UTM}. @{text UTM} is defined as 
+  written @{term UTM}. It is defined as 
   the composition of the Turing machine that packages the arguments and
   the translated recursive 
   function @{text UF}:
 
   \begin{center}
-  @{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"}
+  @{text "UTM \<equiv> arg_coding ; (translate UF)"}
   \end{center}
 
   \noindent
@@ -1656,11 +1587,11 @@
   formula @{term "P \<or> \<not>P"}. For reasoning about computability we need
   to formalise a concrete model of computations. We could have
   followed Norrish \cite{Norrish11} using the $\lambda$-calculus as
-  the starting point for computability theory, but then we would have
+  the starting point for formalising computability theory, but then we would have
   to reimplement on the ML-level his infrastructure for rewriting
   $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that
   can rewrite terms modulo an arbitrary equivalence relation, which
-  Isabelle unfortunately does not yet have.  Even though we would
+  Isabelle unfortunately does not yet have.  Even though, we would
   still need to connect $\lambda$-terms somehow to Turing machines for
   proofs that make essential use of them (for example the
   undecidability proof for Wang's tiling problem \cite{Robinson71}).

Binary file paper.pdf has changed

--- a/scala/ex.scala	Mon Apr 22 10:33:40 2013 +0100
+++ b/scala/ex.scala	Wed Apr 24 09:49:00 2013 +0100
@@ -5,6 +5,16 @@
 import comp1._
 import comp2._
 
+val Lg = {
+ val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
+ val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
+                     Less o (Const(1) o (Id(2, 0), Id(2, 1))))
+ val conR2 = Not o (conR1)
+ Add o (recs.Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
+        recs.Mult o (conR2, Const(0) o (Id(2, 0)))) 
+}
+
+
 
 // Turing machine examples
 val TMCopy = TM((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), 
@@ -65,6 +75,9 @@
 println("Less 4 4:  " + Less.eval(4, 4))
 println("Less 4 6:  " + Less.eval(4, 6))
 println("Less 6 4:  " + Less.eval(6, 4))
+println("Le 4 4:    " + recs.Le.eval(4, 4))
+println("Le 4 6:    " + recs.Le.eval(4, 6))
+println("Le 6 4:    " + recs.Le.eval(6, 4))
 println("Not 0:     " + Not.eval(0))
 println("Not 6:     " + Not.eval(6))
 println("Eq 4 4:    " + Eq.eval(4, 4))
@@ -84,8 +97,16 @@
 println("NextPrime 3: " + NextPrime.eval(3))
 println("NthPrime 1:  " + NthPrime.eval(1))
 println("Listsum [2, 3, 4 , 5, 6]: " + Listsum(5, 4).eval(2, 3, 4, 5, 6))
-println("Strt:  " + Strt(2).eval(2,3))
-
+println("Strt:  " + Strt(2).eval(2, 3))
+println("(<=5) 1: " + (Less o (Id(1, 0), Const(5))).eval(1))
+println("(<=5) 5: " + (Less o (Id(1, 0), Const(5))).eval(5))
+println("(<=5) 6: " + (Less o (Id(1, 0), Const(5))).eval(6))
+println("Max (<=9): " + Maxr(Le o (Id(1, 0), Const(9))).eval(10))
+println("Max (>=9): " + Maxr(Le o (Const(9), Id(1, 0))).eval(8))
+println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(10))
+println("Min (<=9): " + Minr(Le o (Id(1, 0), Const(9))).eval(10))
+println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(8))
+//println("Lg 4 2: " + Lg.eval(4, 2))
 
 // compilation of rec to abacus tests
 def test_comp2(f: Rec, ns: Int*) = {

--- a/scala/recs.scala	Mon Apr 22 10:33:40 2013 +0100
+++ b/scala/recs.scala	Wed Apr 24 09:49:00 2013 +0100
@@ -41,9 +41,19 @@
 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
   override def eval(ns: List[Int]) = 
     if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
-    else throw new IllegalArgumentException("Cn args: " + ns + "," + n)
+    else { 
+      val msg = List("Cn f: " + f, 
+                     "n: " + n,
+                     "f arity: " + f.arity, 
+                     "ns-args: " + ns,
+                     "gs arities: " + gs.map(_.arity).mkString("\n"),
+                     "gs: " + gs.mkString(", ")
+                    )
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
 
   override def arity = n
+  override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
 }
 
 // syntactic convenience
@@ -60,9 +70,18 @@
         g.eval(ns.init ::: List(ns.last - 1, r))
       }
     }
-    else throw new IllegalArgumentException("Pr: args")
+    else {
+      val msg = List("Pr f: " + f, 
+                     "g: " + g,
+                     "n: " + n,
+                     "f arity: " + f.arity,
+                     "g arity: " + g.arity,
+                     "ns-args: " + ns)
+      throw new IllegalArgumentException(msg.mkString("\n"))
+    }
 
   override def arity = n + 1
+  override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
 }
 
 // syntactic convenience
@@ -107,6 +126,7 @@
 val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1)))
 val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1)))
 val Disj = Sign o (Add o (Id(2, 0), Id(2, 1)))
+val Le = Disj o (Less, Eq)
 
 def Nargs(n: Int, m: Int) : List[Rec] = m match {
   case 0 => Nil
@@ -115,6 +135,7 @@
 
 def Sigma(f: Rec) = {
   val ar = f.arity
+  println("sigma f-ar: " + ar)
   Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), 
      Add o (Id(ar + 1, ar), 
             Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1))))))
@@ -140,6 +161,8 @@
 //Definition on page 77 of Boolos's book.
 def Minr(f: Rec) = {
   val ar = f.arity
+  println("f-arity " + ar)
+  println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar)))
   Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar))))))
 }
 
@@ -147,7 +170,7 @@
 def Maxr(f: Rec) = {
   val ar  = f.arity
   val rt  = Id(ar + 1, ar - 1) 
-  val rf1 = Less o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) 
+  val rf1 = Le o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) 
   val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1)))) 
   val Qf  = Not o All(rt, Disj o (rf1, rf2)) 
   Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1)))
@@ -206,12 +229,12 @@
 }
 
 val Lg = {
- val rec_lgR = Less o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
- val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0)), 
-                             Less o (Const(1) o (Id(2, 0)), Id(2, 1))))
- val conR2 = Not o ConR1
+ val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
+ val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), 
+                     Less o (Const(1) o (Id(2, 0), Id(2, 1))))
+ val conR2 = Not o (conR1)
  Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), 
-        Mult o (conR2, Constn(0) o (Id(2, 0)))) 
+        Mult o (conR2, Const(0) o (Id(2, 0)))) 
 }
 
 

--- a/thys/UF.thy	Mon Apr 22 10:33:40 2013 +0100
+++ b/thys/UF.thy	Wed Apr 24 09:49:00 2013 +0100
@@ -533,10 +533,9 @@
   where
   "rec_Minr rf = 
      (let vl = arity rf
-      in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl) 
-              rec_not [Cn (Suc vl) rf 
-                    (get_fstn_args (Suc vl) (vl - 1) @
-                                        [id (Suc vl) (vl)])]) 
+      in let rq = rec_all (id vl (vl - 1)) 
+                  (Cn (Suc vl) rec_not [Cn (Suc vl) rf 
+                    (get_fstn_args (Suc vl) (vl - 1) @ [id (Suc vl) vl])]) 
       in  rec_sigma rq)"
 
 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n"
@@ -766,13 +765,12 @@
   "rec_maxr rr = (let vl = arity rr in 
                   let rt = id (Suc vl) (vl - 1) in
                   let rf1 = Cn (Suc (Suc vl)) rec_le 
-                    [id (Suc (Suc vl)) 
-                     ((Suc vl)), id (Suc (Suc vl)) (vl)] in
+                    [id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in
                   let rf2 = Cn (Suc (Suc vl)) rec_not 
                       [Cn (Suc (Suc vl)) 
                            rr (get_fstn_args (Suc (Suc vl)) 
                             (vl - 1) @ 
-                             [id (Suc (Suc vl)) ((Suc vl))])] in
+                             [id (Suc (Suc vl)) (Suc vl)])] in
                   let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in
                   let Qf = Cn (Suc vl) rec_not [rec_all rt rf]
                   in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @
@@ -1948,10 +1946,8 @@
   where
   "rec_lg = 
   (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
-   let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
-                     [Cn 2 (constn 1) [id 2 0], id 2 0], 
-                            Cn 2 rec_less [Cn 2 (constn 1) 
-                                 [id 2 0], id 2 1]] in 
+   let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0], 
+                              Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in 
    let conR2 = Cn 2 rec_not [conR1] in 
       Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR)
                                                [id 2 0, id 2 1, id 2 0]],