# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358983226 -3600
# Node ID 8c7f10b3da7bf8e882ad7345b13fb330ede2b311
# Parent  2363eb91d9fdccd6d12ebc02770e459b06c1e362
updated

diff -r 2363eb91d9fd -r 8c7f10b3da7b IsaMakefile
--- a/IsaMakefile	Wed Jan 23 20:18:40 2013 +0100
+++ b/IsaMakefile	Thu Jan 24 00:20:26 2013 +0100
@@ -21,7 +21,7 @@
 
 utm: $(OUT)/utm
 
-$(OUT)/utm: *.thy
+$(OUT)/utm: thys/*.thy ROOT.ML
 	@$(USEDIR) -f ROOT.ML -b HOL UTM
 
 paper:  ROOT.ML \
@@ -37,7 +37,7 @@
 session_itp: Paper/ROOT.ML \
 	Paper/document/root* \
 	Paper/*.thy
-	@$(USEDIR) -D generated -f ROOT.ML HOL Paper
+	@$(USEDIR) -D generated -f ROOT.ML UTM Paper
 
 itp: session_itp
 	rm -f Paper/generated/*.aux # otherwise latex will fall over      
diff -r 2363eb91d9fd -r 8c7f10b3da7b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/Paper/Paper.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
+imports "../thys/uncomputable"
 begin
 
 (*
@@ -22,6 +22,7 @@
   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
   update2 ("update") and
   tm_wf0 ("wf") and
+  is_even ("iseven") and
 (*  abc_lm_v ("lookup") and
   abc_lm_s ("set") and*)
   haltP ("stdhalt") and 
@@ -31,6 +32,41 @@
   DUMMY  ("\<^raw:\mbox{$\_$}>")
 
 declare [[show_question_marks = false]]
+
+(* THEOREMS *)
+notation (Rule output)
+  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+
+
 (*>*)
 
 section {* Introduction *}
@@ -52,13 +88,15 @@
 
 
 \noindent
-Suppose you want to mechanise a proof about whether a predicate @{term P}, say, is
+Suppose you want to mechanise a proof for whether a predicate @{term P}, say, is
 decidable or not. Decidability of @{text P} usually amounts to showing
 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
 in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic
 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
 is always provable no matter whether @{text P} is constructed by
-computable means. 
+computable means. We hit this limitation previously when we mechanised the correctness
+proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, 
+but were unable to formalise arguments about computability.
 
 %The same problem would arise if we had formulated
 %the algorithms as recursive functions, because internally in
@@ -183,9 +221,12 @@
 We construct the universal Turing machine from \cite{Boolos87} by
 relating recursive functions to abacus machines and abacus machines to
 Turing machines. Since we have set up in Isabelle/HOL a very general computability
-model and undecidability result, we are able to formalise the
-undecidability of Wang's tiling problem. We are not aware of any other
-formalisation of a substantial undecidability problem.
+model and undecidability result, we are able to formalise other
+results: we describe a proof of the computational equivalence
+of single-sided Turing machines, which is not given in \cite{Boolos87},
+but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation}
+%We are not aware of any other
+%formalisation of a substantial undecidability problem.
 *}
 
 section {* Turing Machines *}
@@ -311,11 +352,11 @@
   %cannot be used as it does not preserve types.} This renaming can be
   %quite cumbersome to reason about. 
   We followed the choice made in \cite{AspertiRicciotti12} 
-  representing a state by a natural number and the states of a Turing
-  machine by the initial segment of natural numbers starting from @{text 0}.
-  In doing so we can compose two Turing machine by
+  representing a state by a natural number and the states in a Turing
+  machine programme by the initial segment of natural numbers starting from @{text 0}.
+  In doing so we can compose two Turing machine programs by
   shifting the states of one by an appropriate amount to a higher
-  segment and adjusting some ``next states'' in the other. {\it composition here?}
+  segment and adjusting some ``next states'' in the other. 
 
   An \emph{instruction} of a Turing machine is a pair consisting of 
   an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
@@ -356,35 +397,26 @@
   the corresponding instruction from the program. For this we define 
   the function @{term fetch}
  
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  \begin{equation}\label{fetch}
+  \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\
   @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\
   \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
   @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\
   \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   \noindent
   In this definition the function @{term nth_of} returns the @{text n}th element
   from a list, provided it exists (@{term Some}-case), or if it does not, it
   returns the default action @{term Nop} and the default state @{text 0} 
-  (@{term None}-case). In doing so we slightly deviate from the description
-  in \cite{Boolos87}: if their Turing machines transition to a non-existing
-  state, then the computation is halted. We will transition in such cases
-  to the @{text 0}-state.\footnote{\it However, with introducing the
-  notion of \emph{well-formed} Turing machine programs we will later exclude such
-  cases and make the  @{text 0}-state the only ``halting state''. A program 
-  @{term p} is said to be well-formed if it satisfies
-  the following three properties:
+  (@{term None}-case). We often need to restrict Turing machine programs 
+  to be well-formed: a program @{term p} is \emph{well-formed} if it 
+  satisfies the following three properties:
 
   \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
-                        & @{text "\<and>"} & @{term "iseven (length p)"}\\
-                        & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
-  \end{tabular}
+  @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
   \end{center}
 
   \noindent
@@ -392,7 +424,6 @@
   state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 
   state, and the third that every next-state is one of the states mentioned in
   the program or being the @{text 0}-state.
-  }
 
   A \emph{configuration} @{term c} of a Turing machine is a state together with 
   a tape. This is written as @{text "(s, (l, r))"}. If we have a 
@@ -425,69 +456,14 @@
   \end{center}
 
   \noindent
-  Recall our definition of @{term fetch} with the default value for
+  Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for
   the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 
   then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
   does not actually halt, but rather transitions to the @{text 0}-state and 
   remains there performing @{text Nop}-actions until @{text n} is reached. 
 
-  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
-  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
-
-  \begin{center}
-  \begin{tabular}{l}
-  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
-  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  where @{text 1} stands for the starting state and @{text 0} for our final state.
-  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
-
-  \begin{center}
-  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
-  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
-  \end{center}
-
-  \noindent
-  Later on we need to consider specific Turing machines that 
-  start with a tape in standard form and halt the computation
-  in standard form. To define a tape in standard form, it is
-  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 
-  that translates lists of natural numbers into tapes. 
-
-  
-  \begin{center}
-  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
-  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
-  \end{tabular}
-  \end{center}
-
-  
-
-
-  By this we mean
-
-  \begin{center}
-  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
-  \end{center}
-
-  \noindent
-  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
-  and the head pointing to the first one; the Turing machine
-  halts with a tape consisting of some @{term Bk}s, followed by a 
-  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
-  The head in the output is pointing again at the first @{term Oc}.
-  The intuitive meaning of this definition is to start the Turing machine with a
-  tape corresponding to a value @{term n} and producing
-  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
-  clustered on the output tape).
-
   Before we can prove the undecidability of the halting problem for Turing machines, 
-  we have to define how to compose two Turing machines. Given our setup, this is 
+  we have to define how to compose two Turing machine programs. Given our setup, this is 
   relatively straightforward, if slightly fiddly. We use the following two
   auxiliary functions:
 
@@ -501,8 +477,8 @@
   \noindent
   The first adds @{text n} to all states, exept the @{text 0}-state,
   thus moving all ``regular'' states to the segment starting at @{text
-  n}; the second adds @{term "length p div 2 + 1"} to the @{text
-  0}-state, thus ridirecting all references to the ``halting state''
+  n}; the second adds @{term "Suc(length p div 2)"} to the @{text
+  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"}
@@ -512,12 +488,26 @@
   \end{center}
 
   \noindent
-  This means @{text "p\<^isub>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"}
-  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'' 
-  an initial segment of the natural numbers.
+  %This means @{text "p\<^isub>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"}
+  %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'' 
+  %an initial segment of the natural numbers.
+
+  In the following we will consider the following Turing machine program
+  that makes a copies a value on the tape.
+
+  \begin{figure}
+  \begin{center}
+  \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
+  @{thm tcopy_init_def} &
+  @{thm tcopy_loop_def} &
+  @{thm tcopy_end_def}
+  \end{tabular}
+  \end{center}
+  \end{figure}
+
 
   \begin{center}
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
@@ -620,6 +610,62 @@
   lambda-terms. For this he introduced a clever rewriting technology
   based on combinators and de-Bruijn indices for
   rewriting modulo $\beta$-equivalence (to keep it manageable)
+
+
+  
+  Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 
+  @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
+
+  \begin{center}
+  \begin{tabular}{l}
+  @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
+  \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  where @{text 1} stands for the starting state and @{text 0} for our final state.
+  A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
+
+  \begin{center}
+  @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
+  \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
+  \end{center}
+
+  \noindent
+  Later on we need to consider specific Turing machines that 
+  start with a tape in standard form and halt the computation
+  in standard form. To define a tape in standard form, it is
+  useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 
+  that translates lists of natural numbers into tapes. 
+
+  
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
+  %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
+  %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
+  \end{tabular}
+  \end{center}
+
+  
+ By this we mean
+
+  \begin{center}
+  %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
+  \end{center}
+
+  \noindent
+  This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
+  and the head pointing to the first one; the Turing machine
+  halts with a tape consisting of some @{term Bk}s, followed by a 
+  ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
+  The head in the output is pointing again at the first @{term Oc}.
+  The intuitive meaning of this definition is to start the Turing machine with a
+  tape corresponding to a value @{term n} and producing
+  a new tape corresponding to the value @{term l} (the number of @{term Oc}s
+  clustered on the output tape).
+
 *}
 
 
diff -r 2363eb91d9fd -r 8c7f10b3da7b Paper/document/root.tex
--- a/Paper/document/root.tex	Wed Jan 23 20:18:40 2013 +0100
+++ b/Paper/document/root.tex	Thu Jan 24 00:20:26 2013 +0100
@@ -37,7 +37,7 @@
 \begin{document}
 
 
-\title{Mechanising Computability Theory in Isabelle/HOL}
+\title{Mechanising Turing Machines and Computability Theory in Isabelle/HOL}
 \author{Jian Xu\inst{1} \and Xingyuan Zhang\inst{1} \and Christian Urban\inst{2}}
 \institute{PLA University of Science and Technology, China \and King's College London, UK}
 
@@ -45,16 +45,20 @@
 
 
 \begin{abstract}
-We present a formalised theory of computability in the 
-theorem prover Isabelle/HOL. This theorem prover is based on classical 
-logic which precludes \emph{direct} reasoning about computability: every 
-boolean predicate is either true or false because of the law of excluded 
-middle. The only way to reason about computability in a classical theorem 
-prover is to formalise a concrete model for computation. 
-We formalise Turing machines and relate them to abacus machines and recursive
-functions. Our theory can be used to formalise other computability results:
-{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
-the notion of a universal Turing machine.}
+We present a formalised theory of computability in the theorem prover
+Isabelle/HOL. This theorem prover is based on classical logic which
+precludes \emph{direct} reasoning about computability: every boolean
+predicate is either true or false because of the law of excluded
+middle. The only way to reason about computability in a classical
+theorem prover is to formalise a concrete model for computation.  We
+formalise Turing machines and relate them to abacus machines and
+recursive functions. We also formalise a universal Turing machine and
+reasoning techniques that allow us to reason about Turing machine
+programs. Our theory can be used to formalise other computability
+results. We give one example about the computational equivalence of 
+single-sided Turing machines. 
+%{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses
+%the notion of a universal Turing machine.}
 \end{abstract}
 
 % generated text of all theories
diff -r 2363eb91d9fd -r 8c7f10b3da7b ROOT.ML
--- a/ROOT.ML	Wed Jan 23 20:18:40 2013 +0100
+++ b/ROOT.ML	Thu Jan 24 00:20:26 2013 +0100
@@ -12,9 +12,10 @@
 *)
   
 no_document 
-use_thys ["thys/turing_basic"(*,
-          "thys/truing_hoare", 
+use_thys ["thys/turing_basic",
+          "thys/turing_hoare", 
 	  "thys/uncomputable", 
 	  "thys/abacus", 
 	  "thys/rec_def", 
-	  "thys/recursive"*)]
+	  "thys/recursive",
+          "thys/UF"]
diff -r 2363eb91d9fd -r 8c7f10b3da7b paper.pdf
Binary file paper.pdf has changed
diff -r 2363eb91d9fd -r 8c7f10b3da7b thys/turing_basic.thy
--- a/thys/turing_basic.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/turing_basic.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -168,16 +168,17 @@
 qed
 
 (* well-formedness of Turing machine programs *)
+abbreviation "is_even n \<equiv> (n::nat) mod 2 = 0"
+
 fun 
   tm_wf :: "tprog \<Rightarrow> bool"
 where
-  "tm_wf (p, off) = (length p \<ge> 2 \<and> length p mod 2 = 0 \<and> 
+  "tm_wf (p, off) = (length p \<ge> 2 \<and> is_even (length p) \<and> 
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2 + off \<and> s \<ge> off))"
 
 abbreviation
   "tm_wf0 p \<equiv> tm_wf (p, 0)"
 
-
 lemma halt_lemma: 
   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 by (metis wf_iff_no_infinite_down_chain)
@@ -349,8 +350,6 @@
   finally show thesis using a by blast
 qed
 
-
-
 lemma tm_comp_fetch_second_zero:
   assumes h1: "fetch B s x = (a, 0)"
   and hs: "tm_wf (A, 0)" "s \<noteq> 0"
@@ -372,7 +371,7 @@
 done 
 
 
-lemma t_merge_second_same:
+lemma tm_comp_second_same:
   assumes a_wf: "tm_wf (A, 0)"
   and steps: "steps0 (1, l, r) B stp = (s', l', r')"
   shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp 
@@ -414,11 +413,11 @@
   ultimately show ?case by blast
 qed
 
-lemma t_merge_second_halt_same:
+lemma tm_comp_second_halt_same:
   assumes "tm_wf (A, 0)"  
   and "steps0 (1, l, r) B stp = (0, l', r')"
   shows "steps0 (Suc (length A div 2), l, r)  (A |+| B) stp = (0, l', r')"
-using t_merge_second_same[OF assms] by (simp)
+using tm_comp_second_same[OF assms] by (simp)
 
 end
 
diff -r 2363eb91d9fd -r 8c7f10b3da7b thys/turing_hoare.thy
--- a/thys/turing_hoare.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/turing_hoare.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -15,32 +15,6 @@
 where
   "P holds_for (s, l, r) = P (l, r)"  
 
-(* halting case *)
-definition
-  Hoare :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
-where
-  "{P} p {Q} \<equiv> 
-     (\<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n)))"
-
-(* not halting case *)
-definition
-  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
-where
-  "{P} p \<up> \<equiv> (\<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n))))"
-
-
-lemma HoareI:
-  assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)"
-  shows "{P} p {Q}"
-unfolding Hoare_def 
-using assms by auto
-
-lemma Hoare_unhaltI:
-  assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)"
-  shows "{P} p \<up>"
-unfolding Hoare_unhalt_def 
-using assms by auto
-
 lemma is_final_holds[simp]:
   assumes "is_final c"
   shows "Q holds_for (steps c p n) = Q holds_for c"
@@ -51,6 +25,35 @@
 apply(auto)
 done
 
+(* Hoare Rules *)
+
+(* halting case *)
+definition
+  Hoare_halt :: "assert \<Rightarrow> tprog0 \<Rightarrow> assert \<Rightarrow> bool" ("({(1_)}/ (_)/ {(1_)})" [50, 49] 50)
+where
+  "{P} p {Q} \<equiv> \<forall>tp. P tp \<longrightarrow> (\<exists>n. is_final (steps0 (1, tp) p n) \<and> Q holds_for (steps0 (1, tp) p n))"
+
+(* not halting case *)
+definition
+  Hoare_unhalt :: "assert \<Rightarrow> tprog0 \<Rightarrow> bool" ("({(1_)}/ (_)) \<up>" [50, 49] 50)
+where
+  "{P} p \<up> \<equiv> \<forall>tp. P tp \<longrightarrow> (\<forall> n . \<not> (is_final (steps0 (1, tp) p n)))"
+
+
+lemma Hoare_haltI:
+  assumes "\<And>l r. P (l, r) \<Longrightarrow> \<exists>n. is_final (steps0 (1, (l, r)) p n) \<and> Q holds_for (steps0 (1, (l, r)) p n)"
+  shows "{P} p {Q}"
+unfolding Hoare_halt_def 
+using assms by auto
+
+lemma Hoare_unhaltI:
+  assumes "\<And>l r n. P (l, r) \<Longrightarrow> \<not> is_final (steps0 (1, (l, r)) p n)"
+  shows "{P} p \<up>"
+unfolding Hoare_unhalt_def 
+using assms by auto
+
+
+
 
 text {*
   {P1} A {Q1}   {P2} B {Q2}  Q1 \<mapsto> P2   A well-formed
@@ -59,20 +62,20 @@
 *}
 
 
-lemma Hoare_plus_halt: 
+lemma Hoare_plus_halt [case_names A_halt B_halt Imp A_wf]: 
   assumes A_halt : "{P1} A {Q1}"
   and B_halt : "{P2} B {Q2}"
   and a_imp: "Q1 \<mapsto> P2"
   and A_wf : "tm_wf (A, 0)"
   shows "{P1} A |+| B {Q2}"
-proof(rule HoareI)
+proof(rule Hoare_haltI)
   fix l r
   assume h: "P1 (l, r)"
   then obtain n1 l' r' 
     where "is_final (steps0 (1, l, r) A n1)"  
       and a1: "Q1 holds_for (steps0 (1, l, r) A n1)"
       and a2: "steps0 (1, l, r) A n1 = (0, l', r')"
-    using A_halt unfolding Hoare_def
+    using A_halt unfolding Hoare_halt_def
     by (metis is_final_eq surj_pair) 
   then obtain n2 
     where "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
@@ -83,10 +86,10 @@
     where "is_final (steps0 (1, l', r') B n3)" 
     and b1: "Q2 holds_for (steps0 (1, l', r') B n3)"
     and b2: "steps0 (1, l', r') B n3 = (0, l'', r'')"
-    using B_halt unfolding Hoare_def 
+    using B_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then have "steps0 (Suc (length A div 2), l', r')  (A |+| B) n3 = (0, l'', r'')"
-    using A_wf by (rule_tac t_merge_second_halt_same) 
+    using A_wf by (rule_tac tm_comp_second_halt_same) 
   ultimately show 
     "\<exists>n. is_final (steps0 (1, l, r) (A |+| B) n) \<and> Q2 holds_for (steps0 (1, l, r) (A |+| B) n)"
     using b1 b2 by (rule_tac x = "n2 + n3" in exI) (simp)
@@ -108,7 +111,7 @@
           {P1} A |+| B  loops
 *}
 
-lemma Hoare_plus_unhalt:
+lemma Hoare_plus_unhalt [case_names A_halt B_unhalt Imp A_wf]:
   assumes A_halt: "{P1} A {Q1}"
   and B_uhalt: "{P2} B \<up>"
   and a_imp: "Q1 \<mapsto> P2"
@@ -121,7 +124,7 @@
     where a: "is_final (steps0 (1, l, r) A n1)" 
     and b: "Q1 holds_for (steps0 (1, l, r) A n1)"
     and c: "steps0 (1, l, r) A n1 = (0, l', r')"
-    using A_halt unfolding Hoare_def 
+    using A_halt unfolding Hoare_halt_def 
     by (metis is_final_eq surj_pair) 
   then obtain n2 where eq: "steps0 (1, l, r) (A |+| B) n2 = (Suc (length A div 2), l', r')"
     using A_wf by (rule_tac tm_comp_pre_halt_same)
@@ -136,7 +139,7 @@
       where "steps0 (Suc 0, l', r') B (n - n2) = (s'', l'', r'')" 
       and "\<not> is_final (s'', l'', r'')" by (metis surj_pair)
     then have "steps0 (Suc (length A div 2), l', r') (A |+| B) (n - n2) = (s''+ length A div 2, l'', r'')"
-      using A_wf by (auto dest: t_merge_second_same simp del: tm_wf.simps)
+      using A_wf by (auto dest: tm_comp_second_same simp del: tm_wf.simps)
     then have "\<not> is_final (steps0 (1, l, r) (A |+| B) (n2 + (n  - n2)))"
       using A_wf by (simp only: steps_add eq) (simp add: tm_wf.simps)
     then show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)" 
@@ -160,13 +163,13 @@
    (simp add: assert_imp_def)
 
 
-lemma Hoare_weak:
+lemma Hoare_weaken:
   assumes a: "{P} p {Q}"
   and b: "P' \<mapsto> P" 
   and c: "Q \<mapsto> Q'"
   shows "{P'} p {Q'}"
 using assms
-unfolding Hoare_def assert_imp_def
+unfolding Hoare_halt_def assert_imp_def
 by (metis holds_for.simps surj_pair)
 
 
diff -r 2363eb91d9fd -r 8c7f10b3da7b thys/uncomputable.thy
--- a/thys/uncomputable.thy	Wed Jan 23 20:18:40 2013 +0100
+++ b/thys/uncomputable.thy	Thu Jan 24 00:20:26 2013 +0100
@@ -57,26 +57,19 @@
 
 (* tcopy_init *)
 
-fun inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-   "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
-
-fun inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where 
-  "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
-
-fun inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
-
-fun inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
-  "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
-
-fun inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
-  where
+fun 
+  inv_init0 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init1 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init2 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init3 :: "nat \<Rightarrow> tape \<Rightarrow> bool" and
+  inv_init4 :: "nat \<Rightarrow> tape \<Rightarrow> bool"
+where
   "inv_init0 x (l, r) = ((x > 1 \<and> l = Oc \<up> (x - 2) \<and> r = [Oc, Oc, Bk, Oc]) \<or>   
                          (x = 1 \<and> l = [] \<and> r = [Bk, Oc, Bk, Oc]))"
+| "inv_init1 x (l, r) = (l = [] \<and> r = Oc \<up> x)"
+| "inv_init2 x (l, r) = (\<exists> i j. i > 0 \<and> i + j = x \<and> l = Oc \<up> i \<and> r = Oc \<up> j)"
+| "inv_init3 x (l, r) = (x > 0 \<and> l = Bk # Oc \<up> x \<and> tl r = [])"
+| "inv_init4 x (l, r) = (x > 0 \<and> ((l = Oc \<up> x \<and> r = [Bk, Oc]) \<or> (l = Oc \<up> (x - 1) \<and> r = [Oc, Bk, Oc])))"
 
 fun inv_init :: "nat \<Rightarrow> config \<Rightarrow> bool"
   where
@@ -184,7 +177,7 @@
     
 lemma init_correct: 
   "x > 0 \<Longrightarrow> {inv_init1 x} tcopy_init {inv_init0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_init1 x (l, r)"
@@ -690,7 +683,7 @@
 
 lemma loop_correct:
   "x > 0 \<Longrightarrow> {inv_loop1 x} tcopy_loop {inv_loop0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_loop1 x (l, r)"
@@ -973,7 +966,7 @@
 
 lemma end_correct:
   "x > 0 \<Longrightarrow> {inv_end1 x} tcopy_end {inv_end0 x}"
-proof(rule_tac HoareI)
+proof(rule_tac Hoare_haltI)
   fix l r
   assume h: "0 < x"
     "inv_end1 x (l, r)"
@@ -1060,7 +1053,7 @@
     by (simp add: assert_imp_def inv_end0.simps tape_of_nl_abv)
   ultimately
   show "{pre_tcopy n} tcopy {post_tcopy n}" 
-    by (rule Hoare_weak)
+    by (rule Hoare_weaken)
 qed
 
 
@@ -1113,7 +1106,7 @@
 
 lemma dither_halts:
   shows "{dither_halt_inv} dither {dither_halt_inv}" 
-apply(rule HoareI)
+apply(rule Hoare_haltI)
 using dither_halt_rs
 apply(auto)
 by (metis (lifting, mono_tags) holds_for.simps is_final_eq prod.cases)
@@ -1314,7 +1307,7 @@
     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc, Oc])"
     using nh_newcase[of "M" "[n]" "1", OF assms] by auto 
   then show "{pre_H_inv M n} H {post_H_halt_inv}"
-    unfolding Hoare_def
+    unfolding Hoare_halt_def
     apply(auto)
     apply(rule_tac x = stp in exI)
     apply(auto)
@@ -1329,7 +1322,7 @@
     where "steps0 (1, Bk \<up> 1, <[code M, n]>) H stp = (0, Bk \<up> i, [Oc])"
     using h_newcase[of "M" "[n]" "1", OF assms] by auto 
   then show "{pre_H_inv M n} H {post_H_unhalt_inv}"
-    unfolding Hoare_def
+    unfolding Hoare_halt_def
     apply(auto)
     apply(rule_tac x = stp in exI)
     apply(auto)
@@ -1387,7 +1380,7 @@
   with assms show "False"
     unfolding P1_def P3_def
     unfolding haltP_def
-    unfolding Hoare_def 
+    unfolding Hoare_halt_def 
     apply(auto)
     apply(erule_tac x = n in allE)
     apply(case_tac "steps0 (Suc 0, [], <[code tcontra]>) tcontra n")