Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a coment about partial_function
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 27 Feb 2013 01:32:53 +0000
changeset 202 7cfc83879fc9
parent 201 09befdf4fc99
child 203 514809bb7ce4
added a coment about partial_function
Paper/Paper.thy file | annotate | diff | comparison | revisions
Paper/document/root.bib file | annotate | diff | comparison | revisions
Paper/document/root.tex file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions 
--- a/Paper/Paper.thy	Tue Feb 26 23:44:57 2013 +0000
+++ b/Paper/Paper.thy	Wed Feb 27 01:32:53 2013 +0000
@@ -89,7 +89,8 @@
   Cn ("Cn\<^isup>_") and
   Mn ("Mn\<^isup>_") and
   rec_calc_rel ("eval") and 
-  tm_of_rec ("translate")
+  tm_of_rec ("translate") and
+  listsum ("\<Sigma>")
 
  
 lemma inv_begin_print:
@@ -172,6 +173,91 @@
 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"
   where
   "clear n e = [Dec n e, Goto 0]"
+
+partial_function (tailrec)
+  run
+where
+  "run p cf = (if (is_final cf) then cf else run p (step0 cf p))"
+
+lemma numeral2:
+  shows "11 = Suc 10"
+  and   "12 = Suc 11"
+  and   "13 = Suc 12"
+  and   "14 = Suc 13"
+  and   "15 = Suc 14"
+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)
+done
+*)
+
 (*>*)
 
 section {* Introduction *}
@@ -233,15 +319,16 @@
 formalisation of Turing machines, as well as abacus machines (a kind
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that Turing machine
-programs can be completely \emph{unstructured}, behaving similar to
-Basic programs containing the infamous goto \cite{Dijkstra68}. This
-precludes in the general case a compositional Hoare-style reasoning
-about Turing programs.  We provide such Hoare-rules for when it
-\emph{is} possible to reason in a compositional manner (which is
-fortunately quite often), but also tackle the more complicated case
-when we translate abacus programs into Turing programs.  This
-reasoning about concrete Turing machine programs is usually
-left out in the informal literature, e.g.~\cite{Boolos87}.
+programs (similarly abacus programs) can be completely
+\emph{unstructured}, behaving similar to Basic programs containing the
+infamous goto \cite{Dijkstra68}. This precludes in the general case a
+compositional Hoare-style reasoning about Turing programs.  We provide
+such Hoare-rules for when it \emph{is} possible to reason in a
+compositional manner (which is fortunately quite often), but also
+tackle the more complicated case when we translate abacus programs
+into Turing programs.  This reasoning about concrete Turing machine
+programs is usually left out in the informal literature,
+e.g.~\cite{Boolos87}.
 
 %To see the difficulties
 %involved with this work, one has to understand that interactive
@@ -606,7 +693,9 @@
   Isabelle/HOL to lift the @{term step}-function in order to realise a
   general evaluation function for Turing machines programs. The reason
   is that functions in HOL-based provers need to be terminating, and
-  clearly there are programs that are not. We can however define a
+  clearly there are programs that are not.\footnote{There is the alternative
+  to use partial functions, which do not necessarily need to terminate, but
+  this does not provide us with a useful induction principle \cite{Krauss10}.} We can however define a
   recursive evaluation function that performs exactly @{text n} steps:
 
   \begin{center}
@@ -1220,10 +1309,16 @@
   This gives us a list of natural numbers specifying how many states
   are needed to translate each abacus instruction. This information
   is needed in order to calculate the state where the Turing machine program
-  of one abacus instruction starts. 
+  of an abacus instruction starts. This can be defined as
 
-  {\it add something here about address}
+  \begin{center}
+  @{thm address.simps[where x="n"]}
+  \end{center}
 
+  \noindent
+  where @{text p} is an abacus program and @{term "take n"} takes the first
+  @{text n} elements from a list.
+  
   The @{text Goto}
   instruction is easiest to translate requiring only one state, namely
   the Turing machine program:
@@ -1245,7 +1340,7 @@
   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\
   @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\
-  \multicolumn{3}{@ {}l@ {}}{\hspace{8mm}@{thm (rhs) findnth.simps(2)}}\\
+  \multicolumn{3}{@ {}l@ {}}{\hspace{6mm}@{thm (rhs) findnth.simps(2)}}\\
   \end{tabular}
   \end{center}
 
--- a/Paper/document/root.bib	Tue Feb 26 23:44:57 2013 +0000
+++ b/Paper/document/root.bib	Wed Feb 27 01:32:53 2013 +0000
@@ -1,4 +1,13 @@
-
+@inproceedings{Krauss10,
+  author    = {A.~Krauss},
+  title     = {{R}ecursive {D}efinitions of {M}onadic {F}unctions},
+  booktitle = {Proc.~of the Workshop on Partiality and Recursion in Interactive
+               Theorem Provers},
+  year      = {2010},
+  pages     = {1-13},
+  series    = {EPTCS},
+  volume    = {43}
+}
 
 @PhdThesis{Myreen09,
   author =	 {M.~O.~Myreen},
--- a/Paper/document/root.tex	Tue Feb 26 23:44:57 2013 +0000
+++ b/Paper/document/root.tex	Wed Feb 27 01:32:53 2013 +0000
@@ -13,8 +13,8 @@
 \usepackage{color}
 
 %% for testing
-\usepackage{endnotes}
-\let\footnote=\endnote
+%\usepackage{endnotes}
+%\let\footnote=\endnote
 
 % urls in roman style, theory text in math-similar italics
 \urlstyle{rm}
Binary file paper.pdf has changed
tm