--- a/Paper/Paper.thy Mon Jan 28 02:38:57 2013 +0000
+++ b/Paper/Paper.thy Tue Jan 29 12:37:06 2013 +0000
@@ -81,10 +81,10 @@
done
lemmas HR1 =
- Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+ Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
lemmas HR2 =
- Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+ Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"]
(*>*)
@@ -180,7 +180,7 @@
%Turing machines.
We are not the first who formalised Turing machines: we are aware
-of the preliminary work by Asperti and Ricciotti
+of the work by Asperti and Ricciotti
\cite{AspertiRicciotti12}. They describe a complete formalisation of
Turing machines in the Matita theorem prover, including a universal
Turing machine. However, they do \emph{not} formalise the undecidability of the
@@ -637,8 +637,8 @@
\end{scope}
\end{tikzpicture}\\[-8mm]\mbox{}
\end{center}
- \caption{The components of the \emph{copy Turing machine} (above). If started
- with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at
+ \caption{The three components of the \emph{copy Turing machine} (above). If started
+ (below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at
the end of the right tape; the second then ``moves'' all @{term Oc}s except the
first from the beginning of the tape to the end; the third ``refills'' the original
block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.}
@@ -662,8 +662,8 @@
\noindent
A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
- leftmost @{term "Oc"} on the tape. Note also that @{text 0} is represented by
- a single filled cell, @{text 1} by two filled cells and so on.
+ leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0}
+ is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.
Before we can prove the undecidability of the halting problem for our
Turing machines, we need to analyse two concrete Turing machine
@@ -728,7 +728,8 @@
It is realatively straightforward to prove that the Turing program
@{term "dither"} shown in \eqref{dither} is correct. This program
should be the ``identity'' when started with a standard tape representing
- @{text "1"} but loop when started with @{text 0} instead.
+ @{text "1"} but loop when started with @{text 0} instead, as pictured
+ below.
\begin{center}
@@ -802,14 +803,14 @@
the following two Hoare-rules for sequentially composed programs.
\begin{center}
- \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}}
- $\inferrule*[Right=@{thm (prem 4) HR1}]
- {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}}
+ \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}
+ $\inferrule*[Right=@{thm (prem 3) HR1}]
+ {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
{@{thm (concl) HR1}}
$ &
$
- \inferrule*[Right=@{thm (prem 4) HR2}]
- {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}}
+ \inferrule*[Right=@{thm (prem 3) HR2}]
+ {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
{@{thm (concl) HR2}}
$
\end{tabular}
@@ -817,18 +818,16 @@
\noindent
The first corresponds to the usual Hoare-rule for composition of two
- terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that
- @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l,
- r)"}. The second rule covers the case where the first program
+ terminating programs. The second rule is for cases where the first program
terminates generating a tape for which the second program loops.
- The side-condition about @{thm (prem 4) HR2} is needed in both rules
+ The side-condition about @{thm (prem 3) HR2} is needed in both rules
in order to ensure that the redirection of the halting and initial
state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
The Hoare-rules above allow us to prove the correctness of @{term tcopy}
by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
- and @{term "tcopy_end"} in isolation. We will show some details for the
+ and @{term "tcopy_end"} in isolation. We will show the details for the
the program @{term "tcopy_begin"}.
--- a/thys/uncomputable.thy Mon Jan 28 02:38:57 2013 +0000
+++ b/thys/uncomputable.thy Tue Jan 29 12:37:06 2013 +0000
@@ -103,47 +103,47 @@
apply(rule_tac inv_begin_step, simp_all)
done
-fun init_state :: "config \<Rightarrow> nat"
+fun begin_state :: "config \<Rightarrow> nat"
where
- "init_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
+ "begin_state (s, l, r) = (if s = 0 then 0 else 5 - s)"
-fun init_step :: "config \<Rightarrow> nat"
+fun begin_step :: "config \<Rightarrow> nat"
where
- "init_step (s, l, r) =
+ "begin_step (s, l, r) =
(if s = 2 then length r else
if s = 3 then (if r = [] \<or> r = [Bk] then 1 else 0) else
if s = 4 then length l
else 0)"
-fun init_measure :: "config \<Rightarrow> nat \<times> nat"
+fun begin_measure :: "config \<Rightarrow> nat \<times> nat"
where
- "init_measure c = (init_state c, init_step c)"
+ "begin_measure c = (begin_state c, begin_step c)"
definition lex_pair :: "((nat \<times> nat) \<times> nat \<times> nat) set"
where
"lex_pair \<equiv> less_than <*lex*> less_than"
-definition init_LE :: "(config \<times> config) set"
+definition begin_LE :: "(config \<times> config) set"
where
- "init_LE \<equiv> (inv_image lex_pair init_measure)"
+ "begin_LE \<equiv> (inv_image lex_pair begin_measure)"
lemma [simp]: "\<lbrakk>tl r = []; r \<noteq> []; r \<noteq> [Bk]\<rbrakk> \<Longrightarrow> r = [Oc]"
by (case_tac r, auto, case_tac a, auto)
-lemma wf_begin_le: "wf init_LE"
-by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def)
+lemma wf_begin_le: "wf begin_LE"
+by(auto intro:wf_inv_image simp:begin_LE_def lex_pair_def)
-lemma init_halt:
+lemma begin_halt:
"x > 0 \<Longrightarrow> \<exists> stp. is_final (steps0 (Suc 0, [], Oc\<up>x) tcopy_begin stp)"
-proof(rule_tac LE = init_LE in halt_lemma)
- show "wf init_LE" by(simp add: wf_begin_le)
+proof(rule_tac LE = begin_LE in halt_lemma)
+ show "wf begin_LE" by(simp add: wf_begin_le)
next
assume h: "0 < x"
show "\<forall>n. \<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<longrightarrow>
(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
- steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+ steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
proof(rule_tac allI, rule_tac impI)
fix n
assume a: "\<not> is_final (steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n)"
@@ -157,25 +157,25 @@
moreover hence "inv_begin x (s, l, r)"
using c b by simp
ultimately show "(steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) (Suc n),
- steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> init_LE"
+ steps (Suc 0, [], Oc \<up> x) (tcopy_begin, 0) n) \<in> begin_LE"
using a
proof(simp del: inv_begin.simps)
assume "inv_begin x (s, l, r)" "0 < s"
- thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> init_LE"
- apply(auto simp: init_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
+ thus "(step (s, l, r) (tcopy_begin, 0), s, l, r) \<in> begin_LE"
+ apply(auto simp: begin_LE_def lex_pair_def step.simps tcopy_begin_def numeral split: if_splits)
apply(case_tac r, auto, case_tac a, auto)
done
qed
qed
qed
-lemma init_correct:
+lemma begin_correct:
"0 < x \<Longrightarrow> {inv_begin1 x} tcopy_begin {inv_begin0 x}"
proof(rule_tac Hoare_haltI)
fix l r
assume h: "0 < x" "inv_begin1 x (l, r)"
hence "\<exists> stp. is_final (steps0 (Suc 0, [], Oc \<up> x) tcopy_begin stp)"
- by (rule_tac init_halt)
+ by (rule_tac begin_halt)
then obtain stp where "is_final (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)" ..
moreover have "inv_begin x (steps (Suc 0, [], Oc\<up>x) (tcopy_begin, 0) stp)"
apply(rule_tac inv_begin_steps)
@@ -913,7 +913,7 @@
shows "{inv_begin1 x} tcopy {inv_end0 x}"
proof -
have "{inv_begin1 x} tcopy_begin {inv_begin0 x}"
- by (metis assms init_correct)
+ by (metis assms begin_correct)
moreover
have "{inv_loop1 x} tcopy_loop {inv_loop0 x}"
by (metis assms loop_correct)
@@ -970,10 +970,10 @@
"dither \<equiv> [(W0, 1), (R, 2), (L, 1), (L, 0)] "
(* invariants of dither *)
-abbreviation
+abbreviation (input)
"dither_halt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
-abbreviation
+abbreviation (input)
"dither_unhalt_inv \<equiv> \<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
lemma dither_loops_aux:
@@ -1083,7 +1083,7 @@
(* invariants *)
def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
- def P3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <1::nat>))"
+ def P3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <1::nat>)"
(*
{P1} tcopy {P2} {P2} H {P3}
@@ -1136,7 +1136,7 @@
(* invariants *)
def P1 \<equiv> "\<lambda>tp. tp = ([]::cell list, <[code_tcontra]>)"
def P2 \<equiv> "\<lambda>tp. tp = ([Bk], <[code_tcontra, code_tcontra]>)"
- def Q3 \<equiv> "\<lambda>tp. (\<exists>n. tp = (Bk \<up> n, <0::nat>))"
+ def Q3 \<equiv> "\<lambda>tp. \<exists>n. tp = (Bk \<up> n, <0::nat>)"
(*
{P1} tcopy {P2} {P2} H {Q3}