--- 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
--- 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).
+
*}
--- 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
--- 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"]
Binary file paper.pdf has changed
--- 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
--- 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)
--- 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")